Commit 2022-12-20 06:34 6bc2e2c8

View on Github →

feat: port Data.Rat.Defs and Data.Rat.Basic (#998) fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

depends on: #996
depends on: #1096

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Rat/Basic.lean

Modified Mathlib/Data/Rat/Defs.lean

added theorem Rat.add_def''

added theorem Rat.coe_int_den

added theorem Rat.coe_int_div_eq_divInt

added theorem Rat.coe_int_eq_divInt

added theorem Rat.coe_int_inj

added theorem Rat.coe_int_num

added theorem Rat.coe_int_num_of_den_eq_one

added theorem Rat.coe_nat_den

added theorem Rat.coe_nat_eq_divInt

added theorem Rat.coe_nat_num

added theorem Rat.den_eq_one_iff

added theorem Rat.den_neg_eq_den

added theorem Rat.den_one

added theorem Rat.den_zero

added theorem Rat.divInt_div_divInt_cancel_left

added theorem Rat.divInt_div_divInt_cancel_right

added theorem Rat.divInt_eq_div

added theorem Rat.divInt_eq_zero

added theorem Rat.divInt_mul_divInt_cancel

added theorem Rat.divInt_ne_zero

added theorem Rat.divInt_ne_zero_of_ne_zero

added theorem Rat.divInt_neg_den

added theorem Rat.divInt_neg_one_one

added theorem Rat.divInt_one_one

added theorem Rat.divInt_zero_one

added theorem Rat.div_num_den

added theorem Rat.eq_iff_mul_eq_mul

added theorem Rat.inv_def'

added theorem Rat.lift_binop_eq

added theorem Rat.mkRat_eq

added theorem Rat.mk_denom_ne_zero_of_ne_zero

added theorem Rat.mk_num_ne_zero_of_ne_zero

added theorem Rat.mul_def'

added theorem Rat.mul_num_den

added theorem Rat.neg_def

added theorem Rat.normalize_eq_mk'

added def Rat.numDenCasesOn'.{u}

added def Rat.numDenCasesOn.{u}

added theorem Rat.num_den'

added theorem Rat.num_den

added theorem Rat.num_div_den

added theorem Rat.num_ne_zero_of_ne_zero

added theorem Rat.num_neg_eq_neg_num

added theorem Rat.num_one

added theorem Rat.num_zero

added theorem Rat.ofInt_eq_cast

added theorem Rat.pos

added theorem Rat.sub_def''

added theorem Rat.zero_iff_num_zero

added theorem Rat.zero_mk

added theorem Rat.zero_of_num_zero