Documentation

Mathlib.Algebra.GroupWithZero.Action.ConjAct

Conjugation action of a group with zero on itself #

source
instance ConjAct.instGroupWithZero {G₀ : Type u_2} [GroupWithZero G₀] :
GroupWithZero (ConjAct G₀)
Equations
source
@[simp]
theorem ConjAct.ofConjAct_zero {G₀ : Type u_2} [GroupWithZero G₀] :
ofConjAct 0 = 0
source
@[simp]
theorem ConjAct.toConjAct_zero {G₀ : Type u_2} [GroupWithZero G₀] :
toConjAct 0 = 0
source
instance ConjAct.mulAction₀ {G₀ : Type u_2} [GroupWithZero G₀] :
MulAction (ConjAct G₀) G₀
Equations
source
instance ConjAct.smulCommClass₀ {α : Type u_1} {G₀ : Type u_2} [GroupWithZero G₀] [SMul α G₀] [SMulCommClass α G₀ G₀] [IsScalarTower α G₀ G₀] :
SMulCommClass α (ConjAct G₀) G₀
source
instance ConjAct.smulCommClass₀' {α : Type u_1} {G₀ : Type u_2} [GroupWithZero G₀] [SMul α G₀] [SMulCommClass G₀ α G₀] [IsScalarTower α G₀ G₀] :
SMulCommClass (ConjAct G₀) α G₀