Commit 2025-01-19 23:29 68ea7d25

View on Github →

chore(Algebra/Order/Floor): Split off round section (#20831) This PR splits the Algebra/Order/Floor.lean file, addressing an instance of a long-file tech debt issue. It does this by moving round and related lemmas to a new file.

Estimated changes

deleted theorem Int.map_round
deleted theorem abs_sub_round
deleted theorem abs_sub_round_eq_min
deleted def round
deleted theorem round_add_int
deleted theorem round_add_nat
deleted theorem round_add_ofNat
deleted theorem round_add_one
deleted theorem round_eq
deleted theorem round_eq_zero_iff
deleted theorem round_intCast
deleted theorem round_int_add
deleted theorem round_le
deleted theorem round_le_add_half
deleted theorem round_natCast
deleted theorem round_nat_add
deleted theorem round_neg_two_inv
deleted theorem round_ofNat
deleted theorem round_ofNat_add
deleted theorem round_one
deleted theorem round_sub_int
deleted theorem round_sub_nat
deleted theorem round_sub_ofNat
deleted theorem round_sub_one
deleted theorem round_two_inv
deleted theorem round_zero
deleted theorem sub_half_lt_round
added theorem Int.map_round
added theorem abs_sub_round
added theorem abs_sub_round_eq_min
added def round
added theorem round_add_int
added theorem round_add_nat
added theorem round_add_ofNat
added theorem round_add_one
added theorem round_eq
added theorem round_eq_zero_iff
added theorem round_intCast
added theorem round_int_add
added theorem round_le
added theorem round_le_add_half
added theorem round_natCast
added theorem round_nat_add
added theorem round_neg_two_inv
added theorem round_ofNat
added theorem round_ofNat_add
added theorem round_one
added theorem round_sub_int
added theorem round_sub_nat
added theorem round_sub_ofNat
added theorem round_sub_one
added theorem round_two_inv
added theorem round_zero
added theorem sub_half_lt_round