Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-03 12:09 c3221f74

View on Github →

feat(data/rat): denom_div_cast_eq_one_iff (#2934)

Estimated changes

Modified src/data/rat/basic.lean

added theorem rat.coe_int_inj

added theorem rat.denom_div_cast_eq_one_iff