finrank_le_one — Mathlib

English

If a module is generated by one vector, then its finrank is 1.

Русский

Если модуль порождается одним вектором, то его finrank равен 1.

LaTeX

$$$$ \\operatorname{finrank}_R M = 1 \\\\text{ if M is generated by one vector}. $$$$

Lean4

/-- If every vector is a multiple of some `v : M`, then `M` has dimension at most one.
-/
theorem finrank_le_one (v : M) (h : ∀ w : M, ∃ c : R, c • v = w) : finrank R M ≤ 1 :=
  by
  haveI := nontrivial_of_invariantBasisNumber R
  rcases eq_or_ne v 0 with (rfl | hn)
  · haveI :=
      _root_.subsingleton_of_forall_eq (0 : M) fun w =>
        by
        obtain ⟨c, rfl⟩ := h w
        simp
    rw [finrank_zero_of_subsingleton]
    exact zero_le_one
  · exact (finrank_eq_one v hn h).le

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