Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-15 15:49 d6b861b0

View on Github →

chore(algebra/order/archimedean): Move material to correct files (#15290) Move round and some floor lemmas to algebra.order.floor. Move the rat.cast lemmas about floor and ceil to data.rat.floor. Merge a few sections together now that unrelated lemmas are gone.

Estimated changes

deleted theorem abs_sub_round
modified theorem archimedean_iff_nat_le
modified theorem archimedean_iff_nat_lt
modified theorem archimedean_iff_rat_le
modified theorem archimedean_iff_rat_lt
modified theorem exists_mem_Ico_zpow
modified theorem exists_mem_Ioc_zpow
modified theorem exists_pow_lt_of_lt_one
modified theorem exists_rat_gt
modified theorem exists_rat_near
deleted theorem rat.cast_fract
deleted theorem rat.ceil_cast
deleted theorem rat.floor_cast
deleted theorem rat.round_cast
deleted def round
deleted theorem round_one
deleted theorem round_zero
deleted theorem sub_floor_div_mul_lt
deleted theorem sub_floor_div_mul_nonneg
added theorem abs_sub_round
added def round
added theorem round_one
added theorem round_zero
added theorem rat.cast_fract
added theorem rat.ceil_cast
added theorem rat.floor_cast
added theorem rat.round_cast