Mathlib Map

Theorems · Definition · number theory

WeakFEPair.g

{E : Type u_1} → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℂ E] → WeakFEPair E → ℝ → E

The functions whose Mellin transform we study

Defined in
Mathlib.NumberTheory.LSeries.AbstractFuncEq
Cited by
13 results in Mathlib
Foundations
Depth 138 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NormedAddCommGroupNormedSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

WeakFEPair.symm · cited by 24WeakFEPair.symmWeakFEPair.h_feq' · cited by 3WeakFEPair.h_feq'WeakFEPair.hg_top · cited by 3WeakFEPair.hg_topWeakFEPair.h_feq · cited by 2WeakFEPair.h_feqWeakFEPair.hf_zero · cited by 2WeakFEPair.hf_zeroWeakFEPair.hg_int · cited by 2WeakFEPair.hg_intIsStrongFEPair.symm_Λ_eq · cited by 2IsStrongFEPair.symm_Λ_eqHurwitzZeta.hurwitzEvenFEPair_zero_symm · cited by 2HurwitzZeta.hurwitzEvenFE…WeakFEPair.g_modif · cited by 1WeakFEPair.g_modifHurwitzZeta.hurwitzOddFEPair_g · cited by 1HurwitzZeta.hurwitzOddFEP…HurwitzZeta.completedCosZeta_eq · cited by 0HurwitzZeta.completedCosZ…WeakFEPair.hf_modif_FE · cited by 0WeakFEPair.hf_modif_FEWeakFEPair.symm_f · cited by 0WeakFEPair.symm_fWeakFEPair.symm_g · cited by 0WeakFEPair.symm_gModularForm.weakFEPair_g · cited by 0ModularForm.weakFEPair_gReal · cited by 25697RealNormedAddCommGroup · cited by 15752NormedAddCommGroupNormedSpace · cited by 12499NormedSpaceComplex · cited by 5565ComplexWeakFEPair · cited by 51WeakFEPairWeakFEPair.gCITED BYCITES

Cites5

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

Cited by15

Results whose statement or proof uses this declaration.