English
Given linearly independent families v and v' in M and M', the combined family obtained via Sum.elim (inl ∘ v) (inr ∘ v') is linearly independent in M × M'.
Русский
Пусть v и v' линейно независимы в M и M'. Тогда объединение через Sum.elim в M×M' остаётся линейно независимым.
LaTeX
$$$\\text{LinearIndependent}_R(\\text{Sum.elim}(\\text{inl}\\circ v)(\\text{inr}\\circ v'))$$$
Lean4
theorem linearIndependent_inl_union_inr' {v : ι → M} {v' : ι' → M'} (hv : LinearIndependent R v)
(hv' : LinearIndependent R v') : LinearIndependent R (Sum.elim (inl R M M' ∘ v) (inr R M M' ∘ v')) :=
by
have :
linearCombination R (Sum.elim (inl R M M' ∘ v) (inr R M M' ∘ v')) =
.prodMap (linearCombination R v) (linearCombination R v') ∘ₗ (sumFinsuppLEquivProdFinsupp R).toLinearMap :=
by ext (_ | _) <;> simp [linearCombination_comapDomain]
rw [LinearIndependent, this]
simpa [LinearMap.coe_prodMap] using ⟨hv, hv'⟩
