Theorem WeakFEPair.hf_zero

Modification history

2026-07-04 15:54

Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean

refactor(LSeries/AbstractFuncEq): `IsStrongFEPair` predicate (#41329) …

Modified WeakFEPair.hf_zero View on Github →

2024-03-20 16:24

Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean

feat(NumberTheory/LSeries): abstract functional equations (#11176) …

Added WeakFEPair.hf_zero View on Github →