Theorem Rat.intCast_num_of_den_eq_one

Modification history

2026-10-27 12:01
Mathlib/Data/Rat/Defs.lean
chore: rename `coe_int` lemmas to `intCast` (#44826) …
Added Rat.intCast_num_of_den_eq_oneView on Github →