Conjugation action of a ring on itself #
@[instance_reducible]
instance
ConjAct.unitsMulSemiringAction
{R : Type u_1}
[Semiring R]
:
MulSemiringAction (ConjAct Rˣ) R
Equations
- ConjAct.unitsMulSemiringAction = { toMulAction := ConjAct.unitsMulDistribMulAction.toMulAction, smul_zero := ⋯, smul_add := ⋯, smul_one := ⋯, smul_mul := ⋯ }