Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-22 14:12 6d2726c6

View on Github →

feat(number_theory/bernoulli): definition and properties of Bernoulli numbers (#6363)

Estimated changes

Modified src/number_theory/bernoulli.lean

added def bernoulli'

added theorem bernoulli'_def'

added theorem bernoulli'_def

added theorem bernoulli'_four

added theorem bernoulli'_odd_eq_zero

added theorem bernoulli'_one

added theorem bernoulli'_power_series

added theorem bernoulli'_spec'

added theorem bernoulli'_spec

added theorem bernoulli'_three

added theorem bernoulli'_two

added theorem bernoulli'_zero

modified def bernoulli

deleted theorem bernoulli_def'

deleted theorem bernoulli_def

added theorem bernoulli_eq_bernoulli'

deleted theorem bernoulli_four

deleted theorem bernoulli_odd_eq_zero

modified theorem bernoulli_one

deleted theorem bernoulli_power_series

deleted theorem bernoulli_spec'

deleted theorem bernoulli_spec

deleted theorem bernoulli_three

deleted theorem bernoulli_two

modified theorem bernoulli_zero

added theorem sum_bernoulli'

modified theorem sum_bernoulli