apply_faithfulSMul — Mathlib

English

The action of RingAut(R) on R is faithful: if two endomorphisms act identically on all elements of R, they are equal.

Русский

Действие RingAut(R) на R верно: если два автоморфизма действуют одинаково на каждом элементе R, то они равны.

LaTeX

$$$\\forall f,g:\\operatorname{RingAut}(R),\\; (\\forall r:\\, R,\\; f(r)=g(r)) \\Rightarrow f=g$$$

Lean4

instance apply_faithfulSMul : FaithfulSMul (RingAut R) R :=
  ⟨RingEquiv.ext⟩

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