Theorems · Theorem · linear algebra

finrank_eq_one

∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] [StrongRankCondition R] (v : M),
  v ≠ 0 → (∀ (w : M), ∃ c, c • v = w) → Module.finrank R M = 1

If there is a nonzero vector and every other vector is a multiple of it, then the module has dimension one.

Defined in

Mathlib.LinearAlgebra.Dimension.Finite

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleIsDomainModule.IsTorsionFreeStrongRankCondition