English
If M and N are linearly disjoint, and at least one of M or N is flat, then the product-family independence holds for all LI families on both sides.
Русский
Если M и N линейно раздельны и хотя бы один из них плоский, то сохраняется линейная независимость семей произведений с обеих сторон.
LaTeX
$$LinearIndependent R (i : κ × ι) ↦ (m i.1).1 * (n i.2).1$$
Lean4
/-- If `M` and `N` are linearly disjoint, if one of `M` and `N` is flat, then for any family of
`R`-linearly independent elements `{ m_i }` of `M`, and any family of
`R`-linearly independent elements `{ n_j }` of `N`, the family `{ m_i * n_j }` in `S` is
also `R`-linearly independent. -/
theorem linearIndependent_mul_of_flat (H : M.LinearDisjoint N) (hf : Module.Flat R M ∨ Module.Flat R N) {κ ι : Type*}
{m : κ → M} {n : ι → N} (hm : LinearIndependent R m) (hn : LinearIndependent R n) :
LinearIndependent R fun (i : κ × ι) ↦ (m i.1).1 * (n i.2).1 :=
by
rcases hf with _ | _
· exact H.linearIndependent_mul_of_flat_left hm hn
· exact H.linearIndependent_mul_of_flat_right hm hn
