reprField — Mathlib

English

The algebra isomorphism applied to an element a ∈ FractionRing (MvPolynomial ι F) coincides with the aeval evaluation.

Русский

Условие совместимости изоморфизма алгебр: применение aeval к элементу FractionRing даёт то же значение, что и соответствующее в hx.reprField.

LaTeX

$$$$ hx.aevalEquivField(a) = IsFractionRing.lift (algebraicIndependent_iff_injective_aeval.2 hx) a. $$$$

Lean4

/-- The canonical map from the intermediate field generated by an algebraic independent family
  into the rational function field. -/
def reprField : IntermediateField.adjoin F (range x) →ₐ[F] FractionRing (MvPolynomial ι F) :=
  hx.aevalEquivField.symm

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