Theorems · Theorem · linear algebra

rank_eq_one_iff

∀ {K : Type u} {V : Type v} [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [Module.Free K V], Module.rank K V = 1 ↔ ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : V), ∃ r, r • v₀ = v

A vector space has dimension 1 if and only if there is a single non-zero vector of which all vectors are multiples.

Defined in

Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Cited by

1 results in Mathlib

Foundations

Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingStrongRankConditionAddCommGroupModuleModule.Free