Theorem ArithmeticFunction.self_mul_dirichletInverse

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