Newton recursion from power sums

Definition

Esgk_NewtonElementaryFromPowerSums

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

algebranumber-theorysymmetric-polynomials

This recursively defines elementary-symmetric quantities from a sequence of power sums using the Newton identity recurrence over a commutative ring containing the rationals.

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Mathlib
import Mathlib.Data.Multiset.Fintype
import Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/


noncomputable section

namespace Esgk

open scoped BigOperators


def newtonElementaryFromPowerSums {A : Type*} [CommRing A] [Algebra ℚ A]
    (P : ℕ → A) : ℕ → A
  | 0 => 1
  | m + 1 =>
      ((m + 1 : ℚ)⁻¹) •
        ((-1 : A) ^ (m + 2) *
          ∑ a ∈ Finset.HasAntidiagonal.antidiagonal m,
            (-1 : A) ^ (m - a.2) *
              newtonElementaryFromPowerSums P (m - a.2) * P (a.2 + 1))
termination_by m => m
decreasing_by omega


end Esgk

View graph