English
Tensor product of linearly independent families is linearly independent over a domain; if hv and hw are linearly independent, then the family i ↦ v_i ⊗ w_j is independent.
Русский
Тензорное произведение линейно независимых семейств линейно независимо над областью; если hv и hw линейно независимы, то семейство i ↦ 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 over domains.
This is true over non-domains if one of the modules is flat.
See `LinearIndependent.tmul_of_flat_left`. -/
theorem tmul_of_isDomain (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_of_isDomain _ _ hv hw).comp (finsuppTensorFinsupp' _ _ _).symm.injective
rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.coe_comp]
congr!
ext i
simp [finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]
