adjoin_eq_top_of_algebra — Mathlib

English

If Algebra.adjoin F S equals the top subalgebra, then adjoin F S equals the top intermediate field.

Русский

Если Algebra.adjoin F S совпадает с верхней подалгеброй, тогда Adjoin F S равняется верхнему полю.

LaTeX

$$$\ Algebra.adjoin F S = \top \Rightarrow IntermediateField.adjoin F S = \top$$$

Lean4

theorem adjoin_eq_top_of_algebra (hS : Algebra.adjoin F S = ⊤) : adjoin F S = ⊤ :=
  top_le_iff.mp (hS.symm.trans_le <| algebra_adjoin_le_adjoin F S)

Похожие утверждения