Commit 2025-03-11 02:02 9231a9df

View on Github →

chore: deprecations for nightly-2025-03-09 (#22778) This PR installs some deprecations to make room for changes in nightly-2025-03-09. This will be short-lived, but perhaps useful nevertheless.

Estimated changes

Modified Mathlib/Algebra/CharZero/Quotient.lean

Modified Mathlib/Algebra/EuclideanDomain/Int.lean

Modified Mathlib/Algebra/Order/Group/Unbundled/Int.lean

deleted theorem Int.emod_lt

added theorem Int.emod_lt_abs

Modified Mathlib/Data/Int/GCD.lean

Modified Mathlib/Data/Int/Init.lean

deleted theorem Int.natAbs_ediv

added theorem Int.natAbs_ediv_of_dvd

Modified Mathlib/Data/Int/Lemmas.lean

added theorem Int.ediv_emod_unique''

deleted theorem Int.ediv_emod_unique'

Modified Mathlib/Data/Int/ModEq.lean

Modified Mathlib/Data/Nat/ModEq.lean

deleted theorem Nat.add_div

Modified Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean

Modified Mathlib/NumberTheory/ClassNumber/AdmissibleAbs.lean

Modified Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean

Modified Mathlib/NumberTheory/LucasLehmer.lean

Modified Mathlib/NumberTheory/Padics/RingHoms.lean