Commit 2022-12-24 07:34 cd2e53a0

View on Github →

feat: port Data.Rat.Lemmas (#1138)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Rat/Lemmas.lean

added theorem Rat.add_den_dvd

added theorem Rat.add_num_den'

added theorem Rat.add_num_den

added theorem Rat.coe_int_div

added theorem Rat.coe_int_div_self

added theorem Rat.coe_nat_div

added theorem Rat.coe_nat_div_self

added theorem Rat.coe_pnatDen

added theorem Rat.den_div_cast_eq_one_iff

added theorem Rat.den_div_eq_of_coprime

added theorem Rat.den_dvd

added theorem Rat.den_mk

added theorem Rat.div_int_inj

added theorem Rat.exists_eq_mul_div_num_and_eq_mul_div_den

added theorem Rat.inv_coe_int_den

added theorem Rat.inv_coe_int_den_of_pos

added theorem Rat.inv_coe_int_num

added theorem Rat.inv_coe_int_num_of_pos

added theorem Rat.inv_coe_nat_den

added theorem Rat.inv_coe_nat_den_of_pos

added theorem Rat.inv_coe_nat_num

added theorem Rat.inv_coe_nat_num_of_pos

added theorem Rat.inv_def''

added theorem Rat.mul_den

added theorem Rat.mul_den_dvd

added theorem Rat.mul_den_eq_num

added theorem Rat.mul_num

added theorem Rat.mul_num_den'

added theorem Rat.mul_self_den

added theorem Rat.mul_self_num

added theorem Rat.num_den_mk

added theorem Rat.num_div_eq_of_coprime

added theorem Rat.num_dvd

added theorem Rat.num_mk

added def Rat.pnatDen

added theorem Rat.pnatDen_eq_iff_den_eq

added theorem Rat.pnatDen_one

added theorem Rat.pnatDen_zero

added theorem Rat.substr_num_den'