eval₂_evalRingHom

Mathlib.Algebra.Polynomial.Bivariate

URI: https://scilib.ai/kg/mathlib#Polynomial.eval₂_evalRingHom

English

The two evaluation constructions agree: eval₂ (evalRingHom x) = evalEval x.

Русский

Две конструкции вычисления совпадают: eval₂ (evalRingHom x) = evalEval x.

LaTeX

$$$ eval₂\\ (evalRingHom\\ x) = evalEval\\ x $$$

Lean4

theorem eval₂_evalRingHom (x : R) : eval₂ (evalRingHom x) = evalEval x := by ext1;
  rw [← coe_evalEvalRingHom, evalEvalRingHom_eq, coe_eval₂RingHom]

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

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

Разделы

Аффилиация

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