English
Tensor product of linearly independent families is linearly independent under flatness on the right.
Русский
Тензорное произведение линейно независимых наборов сохраняет независимость при плоскости справа.
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_right [Module.Flat R N] (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_right hw).comp _ (Equiv.Set.prod _ _).injective :)
