Commit 2026-10-30 16:27 75b1f08d

View on Github →

feat: use IsApply for ArithmeticFunction (#45386)

Estimated changes

Modified Mathlib/NumberTheory/ArithmeticFunction/Defs.lean

deleted theorem ArithmeticFunction.add_apply

deleted theorem ArithmeticFunction.mul_apply

deleted theorem ArithmeticFunction.neg_apply

deleted theorem ArithmeticFunction.one_apply

deleted theorem ArithmeticFunction.smul_apply

deleted theorem ArithmeticFunction.zero_apply

Modified Mathlib/NumberTheory/ArithmeticFunction/LFunction.lean

Modified Mathlib/NumberTheory/ArithmeticFunction/Misc.lean

Modified Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean

Modified Mathlib/NumberTheory/ArithmeticFunction/VonMangoldt.lean

Modified Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean

Modified Mathlib/NumberTheory/LSeries/Dirichlet.lean