English
If A and B are linearly disjoint with A.toSubalgebra ⊔ B.toSubalgebra = ⊤, then any F-basis of A yields an E-basis on B via the left construction.
Русский
Если A и B линейно разобщены и сумма их подалгебр равна ⊤, то F-базис A порождает базис в E по левому конструированию.
LaTeX
$$$(linearDisjoint_iff'.mp H).basisOfBasisLeft H' b$$$
Lean4
/-- If there are `F`-bases `{ u_i }`, `{ v_j }` of `A`, `L`, such that the products
`{ u_i * v_j }` are linearly independent over `F`, then `A` and `L` are linearly disjoint. -/
theorem of_basis_mul' {κ ι : Type*} (a : Basis κ F A) (b : Basis ι F L)
(H : LinearIndependent F fun (i : κ × ι) ↦ (a i.1).1 * algebraMap L E (b i.2)) : A.LinearDisjoint L :=
Subalgebra.LinearDisjoint.of_basis_mul _ _ a
(b.map (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv) H
