finrank_le_one_iff — Mathlib

English

Let V be a finite-dimensional module over K. Then dim_K V ≤ 1 if and only if there exists a vector v in V such that every element of V is a scalar multiple of v.

Русский

Пусть V — конечномерный модуль над полем K. Тогда dim_K V ≤ 1 тогда и только тогда, когда существует вектор v в V, такой что любой вектор пространства является скаляром от v.

LaTeX

$$$\operatorname{finrank} K V \le 1 \\iff \\exists v \in V, \forall w \in V, \exists c \in K, c \cdot v = w$$$

Lean4

/-- A finite-dimensional module has dimension at most 1 iff
there is some `v : V` so every vector is a multiple of `v`.
-/
theorem finrank_le_one_iff [Module.Free K V] [Module.Finite K V] :
    finrank K V ≤ 1 ↔ ∃ v : V, ∀ w : V, ∃ c : K, c • v = w := by
  rw [← rank_le_one_iff, ← finrank_eq_rank, Nat.cast_le_one]

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