finrank_eq_one_iff_of_nonzero' — Mathlib

English

For a nonzero vector v, finrank K V = 1 is equivalent to span K({v}) = top.

Русский

Для ненулевого вектора v размерность пространства равна 1 эквивалентно тому, что span{v} заполнит всё пространство.

LaTeX

$$$\forall v\,(v \neq 0) \Rightarrow (\operatorname{finrank}_K V = 1 \iff \operatorname{span}_K(\{v\}) = \top)$$$

Lean4

/-- A module with a nonzero vector `v` has dimension 1 iff every vector is a multiple of `v`.
-/
theorem finrank_eq_one_iff_of_nonzero' (v : V) (nz : v ≠ 0) : finrank K V = 1 ↔ ∀ w : V, ∃ c : K, c • v = w :=
  by
  rw [finrank_eq_one_iff_of_nonzero v nz]
  apply span_singleton_eq_top_iff

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