Commit 2025-08-28 16:16 c2251e66

View on Github →

chore(Data/Rat/Cast/CharZero): rename Rat.cast_mk to Rat.cast_divInt (#28356) The symbol /. is notation for Rat.divInt, not Rat.mk, so this PR renames Rat.cast_mk to Rat.cast_divInt.

Estimated changes

Modified Mathlib/Data/Rat/Cast/CharZero.lean

added theorem Rat.cast_divInt

deleted theorem Rat.cast_mk

Modified Mathlib/Data/Rat/Defs.lean

modified theorem Rat.intCast_div_eq_divInt

Modified Mathlib/Data/Real/Irrational.lean