finrank_eq_one — Mathlib

English

If M is generated by a single nonzero vector, then finrank_R(M) = rank_R(M) and equals 1.

Русский

Если M порождается одним ненулевым вектором, то finrank_R(M) = rank_R(M) = 1.

LaTeX

$$$$ \\operatorname{finrank}_R M = \\operatorname{rank}_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 finrank_eq_one (v : M) (n : v ≠ 0) (h : ∀ w : M, ∃ c : R, c • v = w) : finrank R M = 1 :=
  finrank_eq_of_rank_eq (rank_eq_one v n h)

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