Conjugation action of a group with zero on itself

@[instance_reducible]

instance ConjAct.instGroupWithZero {G₀ : Type u_2} [GroupWithZero G₀] : GroupWithZero (ConjAct G₀)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ConjAct.ofConjAct_zero {G₀ : Type u_2} [GroupWithZero G₀] : ofConjAct 0 = 0

@[simp]

theorem ConjAct.toConjAct_zero {G₀ : Type u_2} [GroupWithZero G₀] : toConjAct 0 = 0

@[instance_reducible]

instance ConjAct.mulAction₀ {G₀ : Type u_2} [GroupWithZero G₀] : MulAction (ConjAct G₀) G₀

Equations

• ConjAct.mulAction₀ = { toSMul := ConjAct.instSMul, mul_smul := ⋯, one_smul := ⋯ }

instance ConjAct.smulCommClass₀ {α : Type u_1} {G₀ : Type u_2} [GroupWithZero G₀] [SMul α G₀] [SMulCommClass α G₀ G₀] [IsScalarTower α G₀ G₀] : SMulCommClass α (ConjAct G₀) G₀

instance ConjAct.smulCommClass₀' {α : Type u_1} {G₀ : Type u_2} [GroupWithZero G₀] [SMul α G₀] [SMulCommClass G₀ α G₀] [IsScalarTower α G₀ G₀] : SMulCommClass (ConjAct G₀) α G₀