English
In TensorProduct.LinearIndepOn, given hv and hw as LinearIndepOn on sets, the tensor products v_i ⊗ w_j over i ∈ set, j ∈ set form a linearly independent family on product sets under flatness.
Русский
В TensorProduct.LinearIndepOn, если hv и hw являются линейно независимостями на множествах, тензорные произведения v_i ⊗ w_j образуют линейно независимую семью на произведении множеств при плоскостях.
LaTeX
$$$\\forall hv:\\, \\text{LinearIndepOn}_R(v,s),\\; hw:\\, \\text{LinearIndepOn}_R(w,t)\\;\\Rightarrow\\; \\text{LinearIndepOn}_R(\\lambda i : ι × κ, v(i.1) ⊗ w(i.2))\\; (s ×ˢ t)$$$
Lean4
/-- Tensor product of linearly independent families is linearly
independent under some flatness conditions.
The flatness condition could be removed over domains.
See `LinearIndepOn.tmul_of_isDomain`. -/
nonrec theorem tmul_of_flat_left [Module.Flat R M] (hv : LinearIndepOn R v s) (hw : LinearIndepOn R w t) :
LinearIndepOn R (fun i : ι × κ ↦ v i.1 ⊗ₜ[R] w i.2) (s ×ˢ t) :=
((hv.tmul_of_flat_left hw).comp _ (Equiv.Set.prod _ _).injective :)
