English
Tensor product of linearly independent families is linearly independent over flat modules on the right.
Русский
Тензорное произведение линейно независимых наборов линейно независимо по правой модульной плоскости.
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_right [Module.Flat R N] (hv : LinearIndependent R v)
(hw : LinearIndependent R w) : LinearIndependent R fun i : ι × κ ↦ v i.1 ⊗ₜ[R] w i.2 :=
(((TensorProduct.comm R N M).toLinearMap.linearIndependent_iff_of_injOn
(TensorProduct.comm R N M).injective.injOn).mpr
(hw.tmul_of_flat_left hv)).comp
Prod.swap Prod.swap_bijective.injective
