Theorems · Theorem · linear algebra

rank_le_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 : V), ∃ r, r • v₀ = v

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

Defined in

Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingStrongRankConditionAddCommGroupModuleModule.Free