Commit 2025-12-09 14:57 3ac6175c

View on Github →

feat: lemmas about Polynomial.bernoulli and bernoulliFun (#32364) A step towards Euler-Maclaurin. Co-Authored-By: Geoffrey Irving irving@naml.us

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Polynomial/Coeff.lean

added theorem Polynomial.one_add_X_pow_sub_X_pow

Created Mathlib/Analysis/Calculus/ContDiff/Polynomial.lean

added theorem Polynomial.contDiff_aeval

Modified Mathlib/Data/Nat/Choose/Basic.lean

added theorem Nat.add_one_mul_choose_eq

Modified Mathlib/NumberTheory/Bernoulli.lean

added theorem bernoulli'_eq_zero_of_odd

deleted theorem bernoulli'_odd_eq_zero

added theorem bernoulli_eq_zero_of_odd

added theorem bernoulli_two

Modified Mathlib/NumberTheory/BernoulliPolynomials.lean

added theorem Polynomial.bernoulli_comp_neg_X

added theorem Polynomial.bernoulli_comp_one_add_X

added theorem Polynomial.bernoulli_comp_one_sub_X

added theorem Polynomial.bernoulli_eval_neg

added theorem Polynomial.bernoulli_eval_one_sub

added theorem Polynomial.bernoulli_one

added theorem Polynomial.bernoulli_three_eval_one_quarter

added theorem Polynomial.coeff_bernoulli

Modified Mathlib/NumberTheory/ZetaValues.lean

deleted theorem Polynomial.bernoulli_three_eval_one_quarter

added theorem bernoulliFun_eq_integral

added theorem bernoulliFun_eval_half

added theorem bernoulliFun_eval_half_eq_zero

added theorem bernoulliFun_eval_one_sub

added theorem bernoulliFun_mul

added theorem bernoulliFun_one

added theorem bernoulliFun_two

added theorem bernoulliFun_zero

added theorem contDiff_bernoulliFun

added theorem continuous_bernoulliFun

added theorem deriv_bernoulliFun

added theorem integral_bernoulliFun

modified theorem integral_bernoulliFun_eq_zero

added theorem intervalIntegrable_bernoulliFun