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