Commit 2025-10-25 19:37 2d528fd8

View on Github →

chore: deprecate duplicate Rat.{nat,int}Cast_eq_zero and rename _eq_one lemmas (#30868)

Estimated changes

Modified Mathlib/Data/Rat/Defs.lean

deleted theorem Rat.intCast_eq_one

added theorem Rat.intCast_eq_one_iff

deleted theorem Rat.intCast_eq_zero

deleted theorem Rat.natCast_eq_one

added theorem Rat.natCast_eq_one_iff

deleted theorem Rat.natCast_eq_zero

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean