monomial_eq — Mathlib

English

The product over the support of s of X_x^{s_x} equals the monomial s with coefficient 1.

Русский

Произведение X_x^{s_x} по поддержке s равно мономиалу s с коэффициентом 1.

LaTeX

$$$\prod_{x \in s.support} X_x^{s_x} = \mathrm{monomial}(s)(1)$$$

Lean4

theorem monomial_eq : monomial s a = C a * (s.prod fun n e => X n ^ e : MvPolynomial σ R) := by
  simp only [X_pow_eq_monomial, ← monomial_finsupp_sum_index, Finsupp.sum_single]

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