Theorem StrongFEPair.differentiable_Λ

Modification history

2026-07-04 15:54

Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean

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

Deleted StrongFEPair.differentiable_Λ View on Github →

2024-03-20 16:24

Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean

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

Added StrongFEPair.differentiable_Λ View on Github →