spanFinrank_singleton — Mathlib

English

If m ≠ 0 in M, then the span of {m} has spanFinrank equal to 1.

Русский

Если m ≠ 0 в M, то порождаемое {m} подмодуль имеет spanFinrank = 1.

LaTeX

$$$(\operatorname{span}_R(\{m\})).\operatorname{spanFinrank} = 1 \text{ for } m \neq 0.$$$

Lean4

theorem spanFinrank_singleton {m : M} (hm : m ≠ 0) : (span R { m }).spanFinrank = 1 :=
  by
  apply le_antisymm ?_ ?_
  · exact le_trans (Submodule.spanFinrank_span_le_ncard_of_finite (by simp)) (by simp)
  · by_contra!
    simp [Submodule.spanFinrank_eq_zero_iff_eq_bot (fg_span_singleton m), hm] at this

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