algebraMap_aevalEquiv — Mathlib

English

The algebra map from the subalgebra generated by range x to A composed with aevalEquiv agrees with aeval p under evaluation.

Русский

Алгебраическое отображение от подалгебры, порождаемой range x, к A совместно с aevalEquiv совпадает с отображением aeval при применении к p.

LaTeX

$$$\\text{algebraMap} (\\mathrm{Algebra.adjoin}(R, \\mathrm{range}\,x))\\; A\\; (\\text{hx}.\\mathrm{aevalEquiv}\\; p) = \\mathrm{aeval}_x\\; p$$$

Lean4

@[simp]
theorem algebraMap_aevalEquiv (p : MvPolynomial ι R) :
    algebraMap (Algebra.adjoin R (range x)) A (hx.aevalEquiv p) = aeval x p :=
  rfl

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