Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-10 12:55 0f5a1f22

View on Github →

feat(data/rat): Add some lemmas to work with num/denom (#14456)

Estimated changes

Modified src/data/rat/basic.lean

added theorem rat.add_num_denom'

added theorem rat.coe_int_div_eq_mk

added theorem rat.mk_div_mk_cancel_left

added theorem rat.mk_div_mk_cancel_right

added theorem rat.mk_mul_mk_cancel

added theorem rat.mul_num_denom'

added theorem rat.substr_num_denom'