Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-09 03:23 c18a48e9

View on Github →

refactor(data/rat/defs): Use int.cast instead of rat.of_int (#17392) Control the defeq of the has_int_cast ℚ instance.

Estimated changes

deleted theorem rat.cast_of_int
modified theorem rat.cast_one
modified theorem rat.cast_zero
modified theorem rat.coe_int_denom
modified theorem rat.coe_int_eq_mk
deleted theorem rat.coe_int_eq_of_int
modified theorem rat.coe_int_inj
modified theorem rat.coe_int_num
added theorem rat.of_int_eq_cast
deleted theorem rat.of_int_eq_mk