English
If {a_i} is an R-basis of A and {b_j} is an R-basis of B, and the family {a_i * b_j} is R-linearly independent, then A and B are linearly disjoint.
Русский
Если {a_i} — базис A, {b_j} — базис B, и множество {a_i b_j} линейно независимо над R, то A и B линейноDisjoint.
LaTeX
$$$\\text{Basis}_A \\;\\text{basis}_B \\land \\mathrm{LinearIndependent}_R( a_i b_j ) \\Rightarrow A \\perp_L B$$$
Lean4
/-- If `{ a_i }` is an `R`-basis of `A`, if `{ b_j }` is an `R`-basis of `B`,
such that the family `{ a_i * b_j }` in `S` is `R`-linearly independent,
then `A` and `B` are linearly disjoint. -/
theorem of_basis_mul {κ ι : Type*} (a : Basis κ R A) (b : Basis ι R B)
(H : LinearIndependent R fun (i : κ × ι) ↦ (a i.1).1 * (b i.2).1) : A.LinearDisjoint B :=
Submodule.LinearDisjoint.of_basis_mul _ _ a b H
