Theorem ArithmeticFunction.dirichletInverse_mul_self

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.dirichletInverse_mul_selfView on Github →