Commit 2023-05-25 14:31 5611e57a

View on Github →

feat: port NumberTheory.Bernoulli (#4259)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Bernoulli.lean

added def bernoulli'

added def bernoulli'PowerSeries

added theorem bernoulli'PowerSeries_mul_exp_sub_one

added theorem bernoulli'_def'

added theorem bernoulli'_def

added theorem bernoulli'_eq_bernoulli

added theorem bernoulli'_four

added theorem bernoulli'_odd_eq_zero

added theorem bernoulli'_one

added theorem bernoulli'_spec'

added theorem bernoulli'_spec

added theorem bernoulli'_three

added theorem bernoulli'_two

added theorem bernoulli'_zero

added def bernoulli

added def bernoulliPowerSeries

added theorem bernoulliPowerSeries_mul_exp_sub_one

added theorem bernoulli_eq_bernoulli'_of_ne_one

added theorem bernoulli_one

added theorem bernoulli_spec'

added theorem bernoulli_zero

added theorem sum_Ico_pow

added theorem sum_bernoulli'

added theorem sum_bernoulli

added theorem sum_range_pow