applyMulSemiringAction — Mathlib

English

The action of algebra automorphisms on A1 by composition is faithful: if e acts the same on all, then e = identity.

Русский

Действие автоморфизмов на A1 через композицию верно и такое, что если e действует одинаково на всех, то e = 1.

LaTeX

$$$\\text{FaithfulSMul} \\big( (A_1 \\simeq_{R} A_1) , A_1 \\big)$$$

Lean4

/-- The tautological action by `A₁ ≃ₐ[R] A₁` on `A₁`.

This generalizes `Function.End.applyMulAction`. -/
instance applyMulSemiringAction : MulSemiringAction (A₁ ≃ₐ[R] A₁) A₁
    where
  smul := (· <| ·)
  smul_zero := map_zero
  smul_add := map_add
  smul_one := map_one
  smul_mul := map_mul
  one_smul _ := rfl
  mul_smul _ _ _ := rfl

Похожие утверждения