adjoin_eq_top_of_intermediateField

English

If every element of S is algebraic over F and the intermediate field generated by S is top, then the corresponding Algebra.adjoin is top as well.

Русский

Если каждый элемент S алгебраически над F и промежуточное поле, полученное из S, равно верхнему, то Algebra.adjoin F S равно верхнему.

LaTeX

$$Forall (hS : ∀ x ∈ S, IsAlgebraic F x) (hS₂ : IntermediateField.adjoin F S = ⊤), Algebra.adjoin F S = ⊤$$

Lean4

theorem _root_.Algebra.adjoin_eq_top_of_intermediateField {S : Set E} (hS : ∀ x ∈ S, IsAlgebraic F x)
    (hS₂ : IntermediateField.adjoin F S = ⊤) : Algebra.adjoin F S = ⊤ := by
  simp [*, ← IntermediateField.adjoin_algebraic_toSubalgebra hS]

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