English
Tensor product of independent families remains independent over domains; used to deduce independence of tmul in product index.
Русский
Тензорное произведение независимых семейств сохраняет независимость над областями; применяется для независимости tmul в произведении индексов.
LaTeX
$$same as 176234$$
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 `LinearIndepOn.tmul_of_flat_left`. -/
nonrec theorem tmul_of_isDomain (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_isDomain hw).comp _ (Equiv.Set.prod _ _).injective :)
