Theorem Rat.cast_divInt

Modification history

2025-08-28 16:16

Mathlib/Data/Rat/Cast/CharZero.lean

chore(Data/Rat/Cast/CharZero): rename `Rat.cast_mk` to `Rat.cast_divInt` (#28356) …

Added Rat.cast_divInt View on Github →