Commit 2025-08-23 02:29 65d1dd87

View on Github →

feat(*): add Decidable instances (#28765)

Estimated changes

Modified Mathlib/Data/Nat/Prime/Defs.lean

Modified Mathlib/Order/Bounds/Basic.lean

Modified Mathlib/RingTheory/Int/Basic.lean

modified theorem Int.exists_prime_and_dvd

modified theorem Int.prime_iff_natAbs_prime