Commit 2026-08-17 07:49 6d0c9f05

View on Github →

feat: add Bernoulli.dvd_den_bernoulli and related lemmas (#41718) Let p be a prime and k a positive even integer divisible by p-1. We add various results about the divisibility by p of the numerator and denominator of the k-th Bernoulli number. These results are important to build the p-adic zeta function.

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/WithZero.lean

modified theorem WithZero.exp_neg

added theorem WithZero.inv_exp

Modified Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

added theorem WithZero.exp_le_one_iff

added theorem WithZero.exp_lt_one_iff

added theorem WithZero.one_le_exp_iff

added theorem WithZero.one_lt_exp_iff

Modified Mathlib/NumberTheory/Bernoulli.lean

added theorem Bernoulli.dvd_den_bernoulli

added theorem Bernoulli.not_dvd_num_bernoulli

added theorem Bernoulli.not_sq_dvd_den_bernoulli

added theorem Bernoulli.padicValRat_bernoulli

added theorem Bernoulli.padicValuation_bernoulli

Modified Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean

Modified Mathlib/NumberTheory/Padics/ValuativeRel.lean

Modified Mathlib/NumberTheory/RatFunc/Ostrowski.lean

Modified Mathlib/RingTheory/MvPowerSeries/Inverse.lean

deleted theorem MvPowerSeries.inv_eq_zero

Modified Mathlib/RingTheory/PowerSeries/Inverse.lean

deleted theorem PowerSeries.inv_eq_zero

Modified Mathlib/RingTheory/Valuation/Discrete/Basic.lean

Modified Mathlib/RingTheory/Valuation/Discrete/IsDiscreteValuationRing.lean

Modified Mathlib/RingTheory/Valuation/DiscreteValuativeRel.lean