C_mul_X_pow_eq_monomial — Mathlib

English

A variant of the previous result holds when f is a finsupp and g a function into finsupps, expressing the monomial of the sum as a product involving C a and monomials of the components.

Русский

Альтернатива к предыдущему результату: для f и g получаем мономиал суммы как произведение с C a и мономами компонент.

LaTeX

$$$\mathrm{monomial}(f.sum g)\, a = C(a) \cdot \prod_{i} \mathrm{monomial}(g(i))\, 1$$$

Lean4

theorem C_mul_X_pow_eq_monomial {s : σ} {a : R} {n : ℕ} : C a * X s ^ n = monomial (Finsupp.single s n) a := by
  rw [← zero_add (Finsupp.single s n), monomial_add_single, C_apply]

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