Theorems · Definition · number theory
bernoulli
ℕ → ℚ
The Bernoulli numbers are defined to be bernoulli' with a parity sign.
- Defined in
- Mathlib.NumberTheory.Bernoulli
- Cited by
- 42 results in Mathlib
- Foundations
- Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- bernoulli'proof · cited by 23
Cited by44
Results whose statement or proof uses this declaration.
- Polynomial.bernoulliproof · cited by 41
- bernoulli_onestatement · cited by 12
- bernoulli_zerostatement · cited by 11
- bernoulli_eq_bernoulli'_of_ne_onestatement and proof · cited by 10
- Polynomial.bernoulli_zeroproof · cited by 6
- Polynomial.bernoulli_defstatement and proof · cited by 4
- EisensteinSeries.E_qExpansion_coeffstatement and proof · cited by 3
- Polynomial.bernoulli_eval_zerostatement and proof · cited by 3
- hasSum_zeta_natstatement and proof · cited by 3
- bernoulliFun_eval_oneproof · cited by 3
- bernoulliFun_eval_zerostatement and proof · cited by 3
- EisensteinSeries.E_qExpansion_coeff_zeroproof · cited by 2