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₀