nontrivial_of_lt_top — Mathlib

English

If P is a proper submodule of M (i.e., P ≠ M), then the quotient M / P is a nontrivial module; there exists a nonzero coset.

Русский

Если P является proper-подпространством M (то есть P ≠ M), то фактор-модуль M / P не тривиален; существует косет, не равный нулю.

LaTeX

$$$$ P < \\top \\implies \\operatorname{Nontrivial}(M / P). $$$$

Lean4

theorem nontrivial_of_lt_top (h : p < ⊤) : Nontrivial (M ⧸ p) :=
  by
  obtain ⟨x, _, notMem_s⟩ := SetLike.exists_of_lt h
  refine ⟨⟨mk x, 0, ?_⟩⟩
  simpa using notMem_s

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