eval_mul

Mathlib.Algebra.MvPolynomial.Eval

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

English

Let f: σ → R. For polynomials p, q, evaluation respects multiplication: eval f(p q) = eval f(p) · eval f(q).

Русский

Пусть f: σ → R. Для полиномов p, q: eval f(p q) = eval f(p) · eval f(q).

LaTeX

$$$$\operatorname{eval}_f(p q) = \operatorname{eval}_f(p) \cdot \operatorname{eval}_f(q).$$$$

Lean4

theorem eval_mul : eval f (p * q) = eval f p * eval f q :=
  eval₂_mul _ _

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

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

Разделы

Аффилиация

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