English
Tensor product of linearly independent families is linearly independent under flatness; in particular, if v and w are linearly independent families, then the family i ↦ v_i ⊗ w_j over i,j is linearly independent.
Русский
Тензорное произведение линейно независимых наборов сохраняет линейную независимость при плоскости; если v и w образуют линейно независимые наборы, то семейство i,j ↦ v_i ⊗ w_j линейно независимо.
LaTeX
$$$\\forall hv:\\, \\text{LinearIndependent}_R(v),\\; hw:\\, \\text{LinearIndependent}_R(w) \\;\Rightarrow\\; \\text{LinearIndependent}_R (\\lambda i : ι × κ, v(i.1) ⊗ w(i.2))$$$
Lean4
/-- Tensor product of linearly independent families is linearly
independent under some flatness conditions.
The flatness condition could be removed over domains.
See `LinearIndependent.tmul_of_isDomain`. -/
theorem _root_.LinearIndependent.tmul_of_flat_left [Module.Flat R M] (hv : LinearIndependent R v)
(hw : LinearIndependent R w) : LinearIndependent R fun i : ι × κ ↦ v i.1 ⊗ₜ[R] w i.2 :=
by
rw [LinearIndependent]
convert (TensorProduct.map_injective_of_flat_flat _ _ hv hw).comp (finsuppTensorFinsupp' _ _ _).symm.injective
rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.coe_comp]
congr!
ext i
simp [finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]
