Theorem StrongFEPair.functional_equation

Modification history

2026-07-04 15:54

Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean

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

Deleted StrongFEPair.functional_equation View on Github →

2024-03-20 16:24

Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean

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

Added StrongFEPair.functional_equation View on Github →