English
If A and B are linearly disjoint and some basis a of A and basis b of B satisfy that the family {a_i * b_j} is linearly independent, then A and B are linearly disjoint.
Русский
Если A и B линейно параллельны и существует база a для A и база b для B такая, что множество {a_i b_j} линейно независимо, то A и B линейно независимы между собой.
LaTeX
$$$A\\perp_L B \\implies (\\exists \\text{basis } a \\text{ of } A, \\exists \\text{basis } b \\text{ of } B: \\ LinearIndependent_R( (a_i) \\otimes (b_j) ) ) \\Rightarrow A\\perp_L B$$$
Lean4
/-- If `A` and `B` are linearly disjoint, if one of `A` and `B` is flat, then for any family of
`R`-linearly independent elements `{ a_i }` of `A`, and any family of
`R`-linearly independent elements `{ b_j }` of `B`, the family `{ a_i * b_j }` in `S` is
also `R`-linearly independent. -/
theorem linearIndependent_mul_of_flat (H : A.LinearDisjoint B) (hf : Module.Flat R A ∨ Module.Flat R B) {κ ι : Type*}
{a : κ → A} {b : ι → B} (ha : LinearIndependent R a) (hb : LinearIndependent R b) :
LinearIndependent R fun (i : κ × ι) ↦ (a i.1).1 * (b i.2).1 :=
Submodule.LinearDisjoint.linearIndependent_mul_of_flat H hf ha hb
