English
If A and B are linearly disjoint with A.toSubalgebra ⊔ B.toSubalgebra = ⊤, then any F-basis of A is a B-E basis.
Русский
Если A и B линейно разобщены и их сумма подалгебр равна ⊤, то любая F-базис A является базисом B в E.
LaTeX
$$$A \perp_F B \,\Rightarrow\, \text{basis of } A \text{ is a basis of } E$$$
Lean4
/-- If `A` and `B` are linearly disjoint and such that `A.toSubalgebra ⊔ B.toSubalgebra = ⊤`,
then any `F`-basis of `A` is also a `B`-basis of `E`.
Note that the condition `A.toSubalgebra ⊔ B.toSubalgebra = ⊤` is equivalent to
`A ⊔ B = ⊤` in many cases, see `IntermediateField.sup_toSubalgebra_of_isAlgebraic_right` and similar
results.
-/
noncomputable def basisOfBasisLeft (H : A.LinearDisjoint B) (H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤) {ι : Type*}
(b : Basis ι F A) : Basis ι B E :=
(linearDisjoint_iff'.mp H).basisOfBasisLeft H' b
