finrank_eq_one_iff_of_nonzero — Mathlib

English

Let v ∈ V with v ≠ 0. Then finrank_K V = 1 if and only if span_K({v}) = V.

Русский

Пусть v не равен нулю. Тогда finrank_K V = 1 тогда и только тогда, когда span_K({v}) = V.

LaTeX

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

Lean4

/-- A vector space with a nonzero vector `v` has dimension 1 iff `v` spans.
-/
theorem finrank_eq_one_iff_of_nonzero (v : V) (nz : v ≠ 0) : finrank K V = 1 ↔ span K ({ v } : Set V) = ⊤ :=
  ⟨fun h => by simpa using (basisSingleton Unit h v nz).span_eq, fun s =>
    finrank_eq_card_basis (Basis.mk (LinearIndepOn.id_singleton _ nz) (by simp [← s]))⟩

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