eval_monomial — Mathlib

English

There is a direct formula for evaluating a monomial: eval f (monomial s a) = a · ∏ i ∈ s.support, f(i)^{s(i)}.

Русский

Для монома существует явная формула вычисления: eval f (monomial s a) = a · ∏ i ∈ supp(s) f(i)^{s(i)}.

LaTeX

$$$\\mathrm{eval} f (\\mathrm{monomial}(s,a)) = a \\cdot \\prod_{i \\in \\mathrm{supp}(s)} f(i)^{s(i)}$$$

Lean4

theorem eval_monomial : eval f (monomial s a) = a * s.prod fun n e => f n ^ e :=
  eval₂_monomial _ _

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