Theorems · Theorem · linear algebra

exists_linearIndependent_pair_of_one_lt_finrank

∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [HasRankNullity.{u, u_1} R] [StrongRankCondition R] [IsDomain R] [Module.IsTorsionFree R M],
  1 < Module.finrank R M → ∀ {x : M}, x ≠ 0 → ∃ y, LinearIndependent R ![x, y]

Given a nonzero vector in a finite-dimensional space of dimension > 1, one may find another vector linearly independent of the first one.

Defined in

Mathlib.LinearAlgebra.Dimension.RankNullity

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleHasRankNullityStrongRankConditionIsDomainModule.IsTorsionFree