Coefficient splitting for a monomial

Proved

OAI.PiExponent.FormalInterpolation.flattened_coeff_finsupp_monomial

by Eyal1990 · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

For a single multivariate monomial with polynomial coefficient, flattening preserves the coefficient obtained by selecting successor-coordinate exponents first and then the zeroth polynomial exponent.

Preamble

import Definitions.Def_OAI_PiExponent_TruncatedPolynomialJets

open scoped BigOperators
open OAI.PiExponent OAI.PiExponent.FormalInterpolation

Formal statement

theorem OAI.PiExponent.FormalInterpolation.flattened_coeff_finsupp_monomial
    {m : Nat} (p : Polynomial Complex) (d : Fin m →₀ Nat)
    (e : Fin (m + 1) →₀ Nat) :
    (MvPolynomial.eval₂Hom
      (((Polynomial.aeval (MvPolynomial.X (0 : Fin (m + 1)))) :
        Polynomial Complex →ₐ[Complex] MvPolynomial (Fin (m + 1)) Complex).toRingHom)
      (fun i : Fin m => MvPolynomial.X i.succ)
      (MvPolynomial.monomial d p)).coeff e =
      ((MvPolynomial.monomial d p).coeff
        (InterpolationMatrix.exponentVector (fun i => e i.succ))).coeff (e 0) := by sorry

View graph