span_singleton_eq_top — Mathlib

English

In a simple module, the submodule generated by any nonzero element is the whole module.

Русский

В простом модуле подмодуль, порожденный любым ненулевым элементом, равен всему модулю.

LaTeX

$$$\\forall m\\, (hm : m \\neq 0),\\; Submodule.span R \\{ m \\} = \\top$$$

Lean4

theorem span_singleton_eq_top {m : M} (hm : m ≠ 0) : Submodule.span R { m } = ⊤ :=
  (eq_bot_or_eq_top _).resolve_left fun h ↦ hm (h.le <| Submodule.mem_span_singleton_self m)

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