applyFaithfulSMul — Mathlib

English

The action of RingAut(R) on R is faithful; equivalently, RingAut(R) acts on R by evaluation and different automorphisms give different actions on R.

Русский

Действие RingAut(R) на R верно: разные автоморфизмы порождают разные действия на R.

LaTeX

$$$\\operatorname{FaithfulSMul}(\\operatorname{RingAut}(R), R)$$$

Lean4

/-- `RingHom.applyMulSemiringAction` is faithful. -/
instance applyFaithfulSMul : FaithfulSMul (R →+* R) R :=
  ⟨fun {_ _} h => RingHom.ext h⟩

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