apply_faithfulSMul — Mathlib

English

The action of Module.End_R(M) on M is faithful: if f(m) = g(m) for all m ∈ M, then f = g.

Русский

Действие End_R(M) на M верно по первому параметру: если f(m) = g(m) для всех m, то f = g.

LaTeX

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

Lean4

/-- `LinearMap.applyModule` is faithful. -/
instance apply_faithfulSMul : FaithfulSMul (Module.End R M) M :=
  ⟨LinearMap.ext⟩

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