instIsFaithfulEnd — Mathlib

English

The natural representation of the endomorphism algebra End_R(M) on M is faithful.

Русский

Естественное действие алгебры эндоморфизмов End_R(M) на M верно (через отображение каждого эндоморфизма в себя как линейного оператора).

LaTeX

$$$\forall f \in \mathrm{End}_R(M),\; (\forall m \in M, f(m)=0) \Rightarrow f=0$.$$

Lean4

instance : IsFaithful R (Module.End R M) M where injective_toEnd := by simpa using injective_id

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