Commit 2026-03-02 19:44 207001c8

View on Github →

feat(NumberTheory/ArithmeticFunction/Defs): define the Dirichlet inverse of an arithmetic function (#35810) This PR defines the Dirichlet inverse of an arithmetic function.

Estimated changes

Modified Mathlib/NumberTheory/ArithmeticFunction/Defs.lean

added def ArithmeticFunction.dirichletInverse

added def ArithmeticFunction.dirichletInverseFun

added theorem ArithmeticFunction.dirichletInverseFun_apply_ne

added theorem ArithmeticFunction.dirichletInverseFun_apply_one

added theorem ArithmeticFunction.dirichletInverseFun_apply_zero

added theorem ArithmeticFunction.dirichletInverse_mul_self

added theorem ArithmeticFunction.isUnit_iff_isUnit_apply_one

added theorem ArithmeticFunction.self_mul_dirichletInverse