finrank_eq_one_iff' — Mathlib

English

A free module has finrank 1 iff there exists a vector v ≠ 0 such that every vector is a scalar multiple of v.

Русский

Свободный модуль имеет finrank = 1 тогда и только тогда, когда существует вектор v ≠ 0, такой что любой вектор является его скалярным кратным.

LaTeX

$$$$ \\text{finrank}_R M = 1 \\iff \\exists v \\neq 0,\\, \\forall w, \\exists c:\\; c\\,v = w $$$$

Lean4

/-- A module has dimension 1 iff there is some nonzero `v : V` so every vector is a multiple of `v`.
-/
theorem finrank_eq_one_iff' [Module.Free K V] : finrank K V = 1 ↔ ∃ v ≠ 0, ∀ w : V, ∃ c : K, c • v = w :=
  by
  rw [← rank_eq_one_iff]
  exact toNat_eq_iff one_ne_zero

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