English
A submodule has rank 1 iff there exists a nonzero vector in s that spans s.
Русский
Подмодуль имеет ранг 1 тогда и только тогда, когда существует ненулевой в s, который порождает s.
LaTeX
$$$$ \\text{Module.rank }K\\,s = 1 \\iff \\exists v_0 \\in s, v_0 \\neq 0 \\wedge s \\le K \\cdot v_0 $$$$
Lean4
/-- A submodule has dimension `1` if and only if there is a
single non-zero vector in the submodule such that the submodule is contained in
its span. -/
theorem rank_submodule_eq_one_iff (s : Submodule K V) [Module.Free K s] :
Module.rank K s = 1 ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ s ≤ K ∙ v₀ :=
by
simp_rw [rank_eq_one_iff, le_span_singleton_iff]
refine
⟨fun ⟨⟨v₀, hv₀⟩, H, h⟩ ↦ ⟨v₀, hv₀, fun h' ↦ by simp only [h', ne_eq] at H; exact H rfl, fun v hv ↦ ?_⟩,
fun ⟨v₀, hv₀, H, h⟩ ↦ ⟨⟨v₀, hv₀⟩, fun h' ↦ H (by rwa [AddSubmonoid.mk_eq_zero] at h'), fun ⟨v, hv⟩ ↦ ?_⟩⟩
· obtain ⟨r, hr⟩ := h ⟨v, hv⟩
exact ⟨r, by rwa [Subtype.ext_iff, coe_smul] at hr⟩
· obtain ⟨r, hr⟩ := h v hv
exact ⟨r, by rwa [Subtype.ext_iff, coe_smul]⟩
