Commit 2025-07-07 18:08 ba40838f

View on Github →

chore: rename ZMod.natCast_zmod_eq_zero_iff_dvd to ZMod.natCast_eq_zero_iff (#26541) This matches CharP.cast_eq_zero_iff

Estimated changes

Modified Archive/Imo/Imo2024Q2.lean

Modified Archive/Wiedijk100Theorems/FriendshipGraphs.lean

Modified Mathlib/Data/ZMod/Basic.lean

added theorem ZMod.natCast_eq_zero_iff

deleted theorem ZMod.natCast_zmod_eq_zero_iff_dvd

Modified Mathlib/NumberTheory/Fermat.lean

Modified Mathlib/NumberTheory/LucasLehmer.lean

Modified Mathlib/NumberTheory/Padics/RingHoms.lean

Modified Mathlib/NumberTheory/SumFourSquares.lean

Modified Mathlib/NumberTheory/Wilson.lean

Modified Mathlib/RingTheory/Fintype.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean

Modified Mathlib/RingTheory/RootsOfUnity/Minpoly.lean