instNontrivial — Mathlib

English

If M is a nontrivial module, then End_R(M) is nontrivial; there exists an endomorphism f ≠ 0.

Русский

Если модуль M ненулевой, то End_R(M) ненулевой; существует эндоморфизм f ≠ 0.

LaTeX

$$$ \exists f: \mathrm{End}_R(M), \ f \neq 0 $$$

Lean4

instance instNontrivial [Nontrivial M] : Nontrivial (Module.End R M) :=
  by
  obtain ⟨m, ne⟩ := exists_ne (0 : M)
  exact nontrivial_of_ne 1 0 fun p => ne (LinearMap.congr_fun p m)

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