aevalEquivField_algebraMap_apply_coe

English

Canonical isomorphism between the intermediate field adjoin F range x and the rational function field FractionRing (MvPolynomial ι F).

Русский

Каноническое изоморфизм между промежуточным полем, порожденным x, и полем рациональных функций.

LaTeX

$$$$ \text{aevalEquivField} : \text{FractionRing} (\mathrm{MvPolynomial}_{ι} F) \simeq_{F} \; \; \; \; \; \; \; \; \; \; (\mathrm{IntermediateField.adjoin} F (\mathrm{range}\ x)). $$$$

Lean4

theorem aevalEquivField_algebraMap_apply_coe (a : MvPolynomial ι F) :
    hx.aevalEquivField (algebraMap _ _ a) = aeval x a := by simp

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