English
Let S,T ⊆ E. The intermediate field obtained by adjoining S first and then adjoining T, and then restricting scalars to F, equals the intermediate field obtained by adjoining T first and then adjoining S, and then restricting scalars to F. In symbols: adjoin (adjoin F S) T, restricted to F, equals adjoin (adjoin F T) S, restricted to F.
Русский
Пусть S,T ⊆ E. Промежуточное поле, полученное после последовательного объединения S, затем T и ограничения по F, равно полю, полученному после объединения T, затем S и ограничения по F: adjoin (adjoin F S) T ⟂F = adjoin (adjoin F T) S ⟂F.
LaTeX
$$$(\\\\operatorname{adjoin}(\\\\operatorname{adjoin} F S) T).\\\\restrictScalars F = (\\\\operatorname{adjoin}(\\\\operatorname{adjoin} F T) S).\\\\restrictScalars F$$$
Lean4
/-- `F[S][T] = F[T][S]` -/
theorem adjoin_adjoin_comm (T : Set E) :
(adjoin (adjoin F S) T).restrictScalars F = (adjoin (adjoin F T) S).restrictScalars F := by
rw [adjoin_adjoin_left, adjoin_adjoin_left, Set.union_comm]
