English
There is a canonical action of the group RingAut(R) on R by ring isomorphisms: each automorphism acts on R by evaluation, and this furnishes a MulSemiringAction RingAut(R) on R.
Русский
Существует каноническое действие группы RingAut(R) на R посредством кольцевых изоморфизмов: каждый автоморфизм действует на R через применение к элементу, образуя MulSemiringAction RingAut(R) на R.
LaTeX
$$$\\text{MulSemiringAction}\\; (\\mathrm{RingAut}(R))\\; R$$$
Lean4
/-- The tautological action by the group of automorphism of a ring `R` on `R`. -/
instance applyMulSemiringAction : MulSemiringAction (RingAut R) R
where
smul := (· <| ·)
smul_zero := RingEquiv.map_zero
smul_add := RingEquiv.map_add
smul_one := RingEquiv.map_one
smul_mul := RingEquiv.map_mul
one_smul _ := rfl
mul_smul _ _ _ := rfl
