Theorems · Theorem · number theory

ZMod.LFunction_def_odd

∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ},
  Function.Odd Φ →
    ∀ (s : ℂ), ZMod.LFunction Φ s = ↑N ^ (-s) * ∑ j, Φ j * HurwitzZeta.hurwitzZetaOdd (ZMod.toAddCircle j) s

Defined in: Mathlib.NumberTheory.LSeries.ZMod
Cited by: 2 results in Mathlib
Foundations: Depth 305 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NeZero

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites22

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Realstatement · cited by 25,697
Complexstatement and proof · cited by 5,565
Finset.sumstatement and proof · cited by 5,195
Finset.univstatement and proof · cited by 3,473
AddMonoidHomstatement · cited by 3,230
ZModstatement and proof · cited by 1,024
neg_mulproof · cited by 654
AddSubgroup.zmultiplesstatement · cited by 493
mul_addproof · cited by 413
map_negproof · cited by 378
UnitAddCirclestatement · cited by 157

Cited by2

Results whose statement or proof uses this declaration.

ZMod.LFunction_neg_two_mul_nat_sub_oneproof · cited by 1
ZMod.LFunction_eq_completed_div_gammaFactor_oddproof · cited by 1