English
If such a nonzero vector exists generating M, then finrank_R(M) = 1.
Русский
Если существует ненулевой вектор, порождающий M, то finrank_R(M) = 1.
LaTeX
$$$$ \text{If } \\exists v \\in M, v \neq 0 \text{ and } \\forall w \\in M, \\exists c \\in R, c \\cdot v = w, \\text{ then } \\\\operatorname{finrank}_R M = 1. $$$$
Lean4
/-- If there is a nonzero vector and every other vector is a multiple of it,
then the module has dimension one. -/
theorem rank_eq_one (v : M) (n : v ≠ 0) (h : ∀ w : M, ∃ c : R, c • v = w) : Module.rank R M = 1 :=
by
haveI := nontrivial_of_invariantBasisNumber R
obtain ⟨b⟩ := (Basis.basis_singleton_iff.{_, _, u} PUnit).mpr ⟨v, n, h⟩
rw [rank_eq_card_basis b, Fintype.card_punit, Nat.cast_one]
