collinear_iff_rank_le_one — Mathlib

English

If the vector span of a set is finite-dimensional, then the set is collinear if and only if finrank of the vector span is at most 1.

Русский

Если векторное пространство образовано конечномерно, то множество коллинеарно тогда и только тогда, когда размерность векторного разложения не более 1.

LaTeX

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

Lean4

/-- The definition of `Collinear`. -/
theorem collinear_iff_rank_le_one (s : Set P) : Collinear k s ↔ Module.rank k (vectorSpan k s) ≤ 1 :=
  Iff.rfl

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