English
Let A and B be subalgebras of S over R which are linearly disjoint, with B flat over R. If {a_i} is an R-linearly independent family in A and {b_j} is an R-linearly independent family in B, then the family {a_i b_j} indexed by pairs (i, j) is R-linearly independent in S.
Русский
Пусть A и B — подалгебры S над R, линейно независимые; B плоско относительно R. Пусть {a_i}⊆A и {b_j}⊆B линейно независимо над R. Тогда семейство {a_i b_j} в S линейно независимо над R.
LaTeX
$$$A \perp_L B \;\\&\\; \\text{and } \\mathrm{Flat}_R(B) \\\\forall a_i:\\kappa \\to A, \\; ha:\\mathrm{LinearIndependent}_R(a)\\; \\forall b_j:\\iota \\to B, \\; hb:\\mathrm{LinearIndependent}_R(b) \\\\ \\text{the family } (a_i b_j)_{(i,j)\\in \\kappa\\times\\iota} \\text{ is } \\mathrm{LinearIndependent}_R$$$
Lean4
/-- If `A` and `B` are linearly disjoint, if `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_right (H : A.LinearDisjoint B) [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_right H ha hb
