finrank_span_singleton — Mathlib

English

For any nonzero vector v in a finite-dimensional space, the finrank of the span of {v} is 1.

Русский

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

LaTeX

$$$v \neq 0 \Rightarrow \operatorname{finrank}_K(\operatorname{Span} \{v\}) = 1$$$

Lean4

theorem finrank_span_singleton {v : V} (hv : v ≠ 0) : finrank K (K ∙ v) = 1 :=
  by
  apply le_antisymm
  · exact finrank_span_le_card ({ v } : Set V)
  · rw [Nat.succ_le_iff, finrank_pos_iff]
    use ⟨v, mem_span_singleton_self v⟩, 0
    apply Subtype.coe_ne_coe.mp
    simp [hv]

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