English
The natural action of the monoid RingAut(R) of ring automorphisms on R is given by f • a = f(a) for f in RingAut(R) and a in R; this action satisfies the axioms of aMulSemiringAction, i.e., it preserves zero, addition, multiplication, and one, and distributes over multiplication.
Русский
Естественное действие моноида RingAut(R) множителя на R задаётся как f • a = f(a) для f из RingAut(R) и a из R; это действие удовлетворяет аксиомам MulSemiringAction: сохраняет ноль, сложение, умножение и единицу и распределяется по умножению.
LaTeX
$$$\\forall f:\\operatorname{RingAut}(R),\\; \\forall a:\\, R:\\; f \\cdot a = f(a)$$$
Lean4
/-- The tautological action by `R →+* R` on `R`.
This generalizes `Function.End.applyMulAction`. -/
instance applyMulSemiringAction : MulSemiringAction (R →+* R) R
where
smul := (· <| ·)
smul_one := map_one
smul_mul := map_mul
smul_zero := RingHom.map_zero
smul_add := RingHom.map_add
one_smul _ := rfl
mul_smul _ _ _ := rfl
