English
If L is an intermediate field K over F, and E is algebraic over F, then (adjoin E (L:Set K)).toSubalgebra = Algebra.adjoin E (L:Set K).
Русский
Если L — промежуточное поле K над F, и E алгебраическое над F, то адъюнкт над E и L равен адъюнкту над E и L как подалгебре.
LaTeX
$$$(\text{adjoin } E (L : Set K)).toSubalgebra = \operatorname{Algebra.adjoin}_E (L : Set K)$$
Lean4
theorem of_restrictScalars {K L E : Type*} [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E] [Algebra L E]
[IsScalarTower K L E] {E' : IntermediateField L E} (H : (E'.restrictScalars K).FG) : E'.FG :=
by
obtain ⟨s, hs⟩ := H
refine ⟨s, le_antisymm ?_ ?_⟩
· rw [adjoin_le_iff]
exact (subset_adjoin K _).trans_eq congr(($hs : Set E))
· rw [← restrictScalars_le_iff K, ← hs, adjoin_le_iff]
exact subset_adjoin L _