Commit 2025-09-01 11:18 09fbaf12

View on Github →

chore(NumberTheory): review porting notes (#29070) Go through all porting notes in the NumberTheory folder and fix those with an obvious solution.

Estimated changes

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

added theorem ArithmeticFunction.sum_divisorsAntidiagonal_eq_sum_divisors

Modified Mathlib/NumberTheory/Bertrand.lean

Modified Mathlib/NumberTheory/Cyclotomic/Gal.lean

Modified Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean

Modified Mathlib/NumberTheory/Cyclotomic/Rat.lean

Modified Mathlib/NumberTheory/Dioph.lean

Modified Mathlib/NumberTheory/Divisors.lean

Modified Mathlib/NumberTheory/MulChar/Basic.lean

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean

Modified Mathlib/NumberTheory/Zsqrtd/Basic.lean

deleted theorem Zsqrtd.Nonsquare.ns