Theorems · Theorem · number theory
HurwitzZeta.hurwitzZetaEven_neg_two_mul_nat_add_one
∀ (a : UnitAddCircle) (n : ℕ), HurwitzZeta.hurwitzZetaEven a (-2 * (↑n + 1)) = 0
The trivial zeroes of the even Hurwitz zeta function.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 302 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Complexstatement and proof · cited by 5,565
- Nat.cast_oneproof · cited by 2,501
- neg_mulproof · cited by 654
- Nat.cast_addproof · cited by 586
- two_ne_zeroproof · cited by 251
- div_zeroproof · cited by 251
- Function.update_of_neproof · cited by 198
- mul_ne_zeroproof · cited by 178
- UnitAddCirclestatement and proof · cited by 157
- neg_ne_zeroproof · cited by 70
- Complex.Gammaℝproof · cited by 60
- HurwitzZeta.completedHurwitzZetaEvenproof · cited by 30
Cited by2
Results whose statement or proof uses this declaration.
- ZMod.LFunction_neg_two_mul_nat_add_oneproof · cited by 1
- riemannZeta_neg_two_mul_nat_add_oneproof · cited by 0