adjoin_algebraic_toSubalgebra — Mathlib

English

If every element of S is algebraic over F, then the algebra adjoin S coincides with Algebra.adjoin S as subalgebras.

Русский

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

LaTeX

$$adjoin_algebraic_toSubalgebra (∀ x ∈ S, IsAlgebraic F x)$$

Lean4

theorem adjoin_algebraic_toSubalgebra {S : Set E} (hS : ∀ x ∈ S, IsAlgebraic F x) :
    (IntermediateField.adjoin F S).toSubalgebra = Algebra.adjoin F S :=
  adjoin_eq_algebra_adjoin _ _ fun _ ↦ (Algebra.IsIntegral.adjoin fun x hx ↦ (hS x hx).isIntegral).inv_mem

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