English
A variant: rank s ≤ 1 is equivalent to the existence of some v0 with s ≤ span{v0}, without requiring v0 ∈ s.
Русский
Вариант: rank s ≤ 1 эквивалентно существованию v0 с s ≤ span{v0}, без требования v0 ∈ s.
LaTeX
$$$$ (Module.rank\\,K\\,(Subtype (s.mem))) \\le 1 \\iff \\exists v_0, s \\le K \\cdot v_0 $$$$
Lean4
/-- A submodule has dimension at most `1` if and only if there is a
single vector, not necessarily in the submodule, such that the
submodule is contained in its span. -/
theorem rank_submodule_le_one_iff' (s : Submodule K V) [Module.Free K s] : Module.rank K s ≤ 1 ↔ ∃ v₀, s ≤ K ∙ v₀ :=
by
haveI := nontrivial_of_invariantBasisNumber K
constructor
· rw [rank_submodule_le_one_iff]
rintro ⟨v₀, _, h⟩
exact ⟨v₀, h⟩
· rintro ⟨v₀, h⟩
obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := K) (M := s)
simpa [b.mk_eq_rank''] using
b.linearIndependent.map' _ (ker_inclusion _ _ h) |>.cardinal_le_rank.trans (rank_span_le { v₀ })
