adjoin_simple_toSubalgebra_of_integral

English

IsAlgebraic passes to the subtype within the AdjoinAdjoin construction; the subtype is algebraic over F.

Русский

IsAlgebraic переходит к подпредикату внутри конструкции AdjoinAdjoin; подпредикат алгебраически над F.

LaTeX

$$Algebra.IsAlgebraic (Subtype fun x => SetLike.instMembership.mem (Algebra.adjoin F S) x) (Subtype fun x => SetLike.instMembership.mem (IntermediateField.adjoin F S) x)$$

Lean4

theorem adjoin_simple_toSubalgebra_of_integral (hα : IsIntegral F α) : F⟮α⟯.toSubalgebra = Algebra.adjoin F { α } :=
  adjoin_algebraic_toSubalgebra <| by simpa [isAlgebraic_iff_isIntegral]

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