Theorem ArithmeticFunction.isUnit_iff_isUnit_apply_one

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