Def ArithmeticFunction.dirichletInverseFun

Modification history

2026-03-02 19:44
Mathlib/NumberTheory/ArithmeticFunction/Defs.lean
feat(NumberTheory/ArithmeticFunction/Defs): define the Dirichlet inverse of an arithmetic function (#35810) …
Added ArithmeticFunction.dirichletInverseFunView on Github →