sum_C

Mathlib.Algebra.MvPolynomial.Basic

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

English

The product over the support of s of X_x raised to s_x equals the monomial s with coefficient 1.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem sum_C {A : Type*} [AddCommMonoid A] {b : (σ →₀ ℕ) → R → A} (w : b 0 0 = 0) : sum (C a) b = b 0 a :=
  sum_monomial_eq w

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

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

Разделы

Аффилиация

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