Mathlib Map

Theorems · Inductive type · number theory

IsStrongFEPair

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

A strong FE-pair is a weak FE-pair in which f₀ and g₀ are zero.

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.

HurwitzZeta.isStrong_hurwitzOddFEPair · cited by 6HurwitzZeta.isStrong_hurw…IsStrongFEPair.Λ_eq · cited by 6IsStrongFEPair.Λ_eqIsStrongFEPair.differentiable_Λ · cited by 3IsStrongFEPair.differenti…IsStrongFEPair.hf₀ · cited by 3IsStrongFEPair.hf₀IsStrongFEPair.hg₀ · cited by 3IsStrongFEPair.hg₀CuspForm.isStrongFEPair · cited by 2CuspForm.isStrongFEPairWeakFEPair.isStrongFEPair_toStrongFEPair · cited by 2WeakFEPair.isStrongFEPair…IsStrongFEPair.symm · cited by 2IsStrongFEPair.symmIsStrongFEPair.symm_Λ_eq · cited by 2IsStrongFEPair.symm_Λ_eqisStrongFEPair_symm · cited by 1isStrongFEPair_symmIsStrongFEPair.casesOn · cited by 0IsStrongFEPair.casesOnIsStrongFEPair.hasMellin · cited by 0IsStrongFEPair.hasMellinIsStrongFEPair.hf_top · cited by 0IsStrongFEPair.hf_topIsStrongFEPair.hf_zero · cited by 0IsStrongFEPair.hf_zeroIsStrongFEPair.recOn · cited by 0IsStrongFEPair.recOnNormedAddCommGroup · cited by 15752NormedAddCommGroupNormedSpace · cited by 12499NormedSpaceComplex · cited by 5565ComplexWeakFEPair · cited by 51WeakFEPairIsStrongFEPairCITED BYCITES

Cites4

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.