instNontrivialId — Mathlib

English

Let M be a nontrivial topological module over a semiring R. Then there exists a nonzero continuous linear endomorphism of M, i.e., End_R(M) is nontrivial.

Русский

Пусть M — ненулевая топологическая модуль над полем/полукольцом R. Тогда существует непрерывный линейный эндоморфизм M → M, отличный от нуля, т.е. End_R(M) не тривиален.

LaTeX

$$$\\exists f \\in \\operatorname{End}_R(M) \\setminus \\{0\\}.$$$

Lean4

instance [Nontrivial M₁] : Nontrivial (M₁ →L[R₁] M₁) :=
  ⟨0, 1, fun e ↦
    have ⟨x, hx⟩ := exists_ne (0 : M₁);
    hx (by simpa using DFunLike.congr_fun e.symm x)⟩

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