eval_mul

Mathlib.Algebra.Polynomial.Eval.Defs

URI: https://scilib.ai/kg/mathlib#Polynomial.eval_mul

English

Evaluation is multiplicative: (p q).eval x = p.eval x · q.eval x.

Русский

Оценка по аргументу сохраняет произведение: (p q).eval x = p.eval x · q.eval x.

LaTeX

$$$$ (p q).eval x = p.eval x \\cdot q.eval x $$$$

Lean4

@[simp]
theorem eval_mul : (p * q).eval x = p.eval x * q.eval x :=
  eval₂_mul _ _

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

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

Разделы

Аффилиация

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