sum_monomial_eq — Mathlib

English

Summing a polynomial against monomials recovers the original polynomial.

Русский

Суммирование полинома по мономиалам восстанавливает исходный полином.

LaTeX

$$@[simp] theorem sum_monomial_eq : ∀ p : R[X], (p.sum fun n a => monomial n a) = p$$

Lean4

@[simp]
theorem sum_monomial_eq : ∀ p : R[X], (p.sum fun n a => monomial n a) = p
  | ⟨_p⟩ => (ofFinsupp_sum _ _).symm.trans (congr_arg _ <| Finsupp.sum_single _)

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