Commit 2023-01-10 18:28 1d28dadf

View on Github →

feat: port Data.Rat.Floor (#1418)

depends on: #1304
depends on: #1422
depends on: #1427

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Rat/Floor.lean

added theorem Int.mod_nat_eq_sub_mul_floor_rat_div

added theorem Nat.coprime_sub_mul_floor_rat_div_of_coprime

added theorem Rat.cast_fract

added theorem Rat.ceil_cast

added theorem Rat.floor_cast

added theorem Rat.floor_int_div_nat_eq_div

added theorem Rat.fract_inv_num_lt_num_of_pos

added theorem Rat.num_lt_succ_floor_mul_den

added theorem Rat.round_cast