English
If A and B are linearly disjoint and A.toSubalgebra ⊔ B.toSubalgebra = ⊤, then any F-basis of B is an A-basis of E.
Русский
Если A и B линейно разобщены и сумма их подалгебр равна ⊤, то любая F-базис B является базисом A в E.
LaTeX
$$$A \perp_F B, \; A_{\mathrm{toSubalgebra}} \sqcup B_{\mathrm{toSubalgebra}} = \top \;\Rightarrow\; \text{basis of } B \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 `B` is also an `A`-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 basisOfBasisRight (H : A.LinearDisjoint B) (H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤) {ι : Type*}
(b : Basis ι F B) : Basis ι A E :=
(linearDisjoint_iff'.mp H).basisOfBasisRight H' b
