Commit 2026-05-07 16:32 728fb0b4

View on Github →

chore(NumberTheory/ArithmeticFunction/Misc): protect ArithmeticFunction.id (#39021) …to avoid a clash with _root_.id.

Estimated changes

Modified Mathlib/NumberTheory/ArithmeticFunction/Misc.lean

deleted def ArithmeticFunction.id

modified theorem ArithmeticFunction.id_apply

modified theorem ArithmeticFunction.isMultiplicative_id

modified theorem ArithmeticFunction.pow_one_eq_id