aeval_eq_eval₂Hom

Mathlib.Algebra.MvPolynomial.Eval

URI: https://scilib.ai/kg/mathlib#MvPolynomial.aeval_eq_eval₂Hom

English

The underlying ring hom of aeval f is the same as the evaluation map by f: RingHom (MvPolynomial) = evaluation map.

Русский

Подлежащее приведение аeval f к кольцу совпадает с отображением оценки по f.

LaTeX

$$$\\\\text{coe}(aeval f) = eval f$$$

Lean4

theorem aeval_eq_eval₂Hom (p : MvPolynomial σ R) : aeval f p = eval₂Hom (algebraMap R S₁) f p :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru