Theorems · Theorem · number theory
LSeries_delta
LSeries LSeries.delta = 1
The L-series of δ is the constant function 1.
- Defined in
- Mathlib.NumberTheory.LSeries.Basic
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 194 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- SummationFilter.unconditionalproof · cited by 2,068
- tsumproof · cited by 1,148
- LSeriesstatement · cited by 77
- LSeries.deltastatement · cited by 12
- tsum_ite_eqproof · cited by 8
- LSeries.term_deltaproof · cited by 1
Cited by3
Results whose statement or proof uses this declaration.
- DirichletCharacter.LSeries_twist_vonMangoldt_eqproof · cited by 2
- ArithmeticFunction.LSeries_zeta_mul_Lseries_moebiusproof · cited by 2
- DirichletCharacter.LSeries.mul_mu_eq_oneproof · cited by 1