Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-10 02:23 05d3955a

View on Github →

feat(number_theory/bernoulli): bernoulli_power_series (#6456) Co-authored-by Ashvni Narayanan

Estimated changes

Modified src/data/finset/nat_antidiagonal.lean

added theorem finset.nat.antidiagonal_congr

Modified src/number_theory/bernoulli.lean

added theorem bernoulli'_eq_bernoulli

added def bernoulli'_power_series

deleted theorem bernoulli'_power_series

added theorem bernoulli'_power_series_mul_exp_sub_one

added def bernoulli_power_series

added theorem bernoulli_power_series_mul_exp_sub_one

added theorem bernoulli_spec'