Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-08 08:51 2b68801b

View on Github →

refactor(number_theory/bernoulli_polynomials): improve names (#11805) Cleanup the bernoulli_polynomials file

Estimated changes

Modified src/number_theory/bernoulli_polynomials.lean

deleted theorem bernoulli_poly.bernoulli_poly_eval_one

deleted theorem bernoulli_poly.bernoulli_poly_eval_zero

deleted theorem bernoulli_poly.bernoulli_poly_zero

deleted theorem bernoulli_poly.exp_bernoulli_poly'

deleted theorem bernoulli_poly.sum_bernoulli_poly

deleted def bernoulli_poly

deleted theorem bernoulli_poly_def

added def polynomial.bernoulli

added theorem polynomial.bernoulli_def

added theorem polynomial.bernoulli_eval_one

added theorem polynomial.bernoulli_eval_zero

added theorem polynomial.bernoulli_generating_function

added theorem polynomial.bernoulli_zero

added theorem polynomial.sum_bernoulli