Theorems · Theorem · linear algebra

LinearIndepOn.union_of_quotient

∀ {R : Type u} {M : Type v} {ι : Type w} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {s t : Set ι}
  {f : ι → M},
  LinearIndepOn R f s → LinearIndepOn R (⇑(Submodule.span R (f '' s)).mkQ ∘ f) t → LinearIndepOn R f (s ∪ t)

Defined in

Mathlib.LinearAlgebra.Dimension.Constructions

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModule