algebraicClosure — Mathlib

English

Canonical map from the intermediate adjoin field into the rational function field given by hx.aevalEquivField.

Русский

Каноническое отображение от промежуточного поля к рациональному полю функций, заданное hx.aevalEquivField.

LaTeX

$$$$ hx.aevalEquivField : FractionRing (MvPolynomial ι F) \to ^{F} (Subtype fun x => \dots) $$$$

Lean4

protected theorem algebraicClosure {F E : Type*} [Field F] [Field E] [Algebra F E] {x : ι → E}
    (hx : AlgebraicIndependent F x) : AlgebraicIndependent (algebraicClosure F E) x :=
  hx.extendScalars _

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