Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-07 17:19 b25994d5

View on Github →

feat(number_theory/bernoulli): definition and properties of Bernoulli polynomials (#6309) The Bernoulli polynomials and its properties are defined.

Estimated changes

Modified src/algebra/big_operators/intervals.lean

Modified src/data/finset/basic.lean

added theorem finset.mem_range_le

added theorem finset.mem_range_sub_ne_zero

Created src/number_theory/bernoulli_polynomials.lean

added theorem bernoulli_poly.bernoulli_poly_eval_zero

added theorem bernoulli_poly.bernoulli_poly_zero

added theorem bernoulli_poly.exp_bernoulli_poly'

added theorem bernoulli_poly.sum_bernoulli_poly

added def bernoulli_poly

added theorem bernoulli_poly_def