collinear_iff_finrank_le_one — Mathlib

English

A set is collinear if and only if finrank of its vectorSpan is at most 1, under finite-dimensional hypothesis.

Русский

Снова: коллинеарность эквивалентна тому, что размерность векторного разложения не превосходит 1, при условии конечномерности.

LaTeX

$$$\operatorname{Collinear}_k(s) \iff \operatorname{finrank}_k(\operatorname{vectorSpan}_k(s)) \le 1$$$

Lean4

/-- A set of points, whose `vectorSpan` is finite-dimensional, is
collinear if and only if their `vectorSpan` has dimension at most
`1`. -/
theorem collinear_iff_finrank_le_one {s : Set P} [FiniteDimensional k (vectorSpan k s)] :
    Collinear k s ↔ finrank k (vectorSpan k s) ≤ 1 :=
  by
  have h := collinear_iff_rank_le_one k s
  rw [← finrank_eq_rank] at h
  exact mod_cast h

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