Theorems · Theorem · linear algebra

Pi.linearIndependent_single

∀ {R : Type u_2} {η : Type u_4} {ιs : η → Type u_5} {Ms : η → Type u_6} [inst : Semiring R]
  [inst_1 : (i : η) → AddCommMonoid (Ms i)] [inst_2 : (i : η) → Module R (Ms i)] [inst_3 : DecidableEq η]
  (v : (j : η) → ιs j → Ms j),
  (∀ (i : η), LinearIndependent R (v i)) → LinearIndependent R fun ji => Pi.single ji.fst (v ji.fst ji.snd)

Defined in

Mathlib.LinearAlgebra.StdBasis

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleDecidableEq