prod_X_pow_eq_monomial — Mathlib

English

The finite-sum decomposition of a monomial equals the product of a constant and monomials of its components.

Русский

Декомпозиция монома в виде конечного произведения и мономов компонентов.

LaTeX

$$$\mathrm{monomial}(a_1+a_2) = C(a) \prod \mathrm{monomial}(a_i) 1$$$

Lean4

@[simp]
theorem prod_X_pow_eq_monomial : ∏ x ∈ s.support, X x ^ s x = monomial s (1 : R) := by
  simp only [monomial_eq, map_one, one_mul, Finsupp.prod]

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