Homogeneous Multiset Sum eq hsymm

Proved

D1Bound5.homogeneousMultisetSum_eq_hsymm

by tp · Oct 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-tuplesnumber-theory

The multiset sum agrees at every degree with mathlib's hsymm under evaluation.

Preamble

import Mathlib.Data.Sym.Basic
import Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
import Definitions.Def_D1Bound5_HomogeneousSymmetric_Definitions

Formal statement

section
open Finset Multiset Sym

namespace D1Bound5




theorem _root_.D1Bound5.homogeneousMultisetSum_eq_hsymm
    {ι R : Type*} [Fintype ι] [DecidableEq ι] [CommSemiring R]
    (a : ι → R) (n : ℕ) :
    homogeneousMultisetSum a n =
      MvPolynomial.aeval a (MvPolynomial.hsymm ι R n) := by sorry











end D1Bound5
end

Source

D1Bound5/HomogeneousSymmetric.lean, lines 15-25, SHA-256 9ca0c1b5630feef5d0a34c972d9c43d84be51f3ce74b855f5c9873ea76bd8466. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph