Commit 2025-04-05 12:43 f329753c

View on Github →

chore: split Algebra.Order.Floor (hybrid approach) (#23692) This is a combination of #23662 and #23652. There is an Algebra.Order.Floor.Defs file imported by .Semiring (Nat-valued floor/ceil) and .Ring (Int-valued floor/ceil and fractional part) files.

Estimated changes

added def FloorRing.ofCeil
added def Int.ceil
added theorem Int.ceil_int
added theorem Int.ceil_le
added theorem Int.ceil_nonneg
added theorem Int.ceil_pos
added theorem Int.ceil_toNat
added def Int.floor
added theorem Int.floorRing_ceil_eq
added theorem Int.floorRing_floor_eq
added theorem Int.floor_int
added theorem Int.floor_le
added theorem Int.floor_lt
added theorem Int.floor_nonneg
added theorem Int.floor_nonpos
added theorem Int.floor_toNat
added def Int.fract
added theorem Int.fract_int
added theorem Int.gc_ceil_coe
added theorem Int.gc_coe_floor
added theorem Int.le_ceil
added theorem Int.le_floor
added theorem Int.lt_ceil
added def Nat.ceil
added theorem Nat.ceil_int
added theorem Nat.ceil_le
added theorem Nat.ceil_nat
added theorem Nat.ceil_pos
added def Nat.floor
added theorem Nat.floor_int
added theorem Nat.floor_nat
added theorem Nat.gc_ceil_coe
added theorem Nat.le_floor
added theorem Nat.le_floor_iff
added theorem Nat.lt_ceil
deleted def FloorRing.ofCeil
deleted def FloorRing.ofFloor
deleted def Int.ceil
deleted theorem Int.ceil_int
deleted theorem Int.ceil_le
deleted theorem Int.ceil_nonneg
deleted theorem Int.ceil_pos
deleted theorem Int.ceil_toNat
deleted def Int.floor
deleted theorem Int.floorRing_ceil_eq
deleted theorem Int.floorRing_floor_eq
deleted theorem Int.floor_int
deleted theorem Int.floor_le
deleted theorem Int.floor_lt
deleted theorem Int.floor_nonneg
deleted theorem Int.floor_nonpos
deleted theorem Int.floor_toNat
deleted def Int.fract
deleted theorem Int.fract_int
deleted theorem Int.gc_ceil_coe
deleted theorem Int.gc_coe_floor
deleted theorem Int.le_ceil
deleted theorem Int.le_floor
deleted theorem Int.lt_ceil
deleted theorem Nat.add_one_le_ceil_iff
deleted def Nat.ceil
deleted theorem Nat.ceil_add_le
deleted theorem Nat.ceil_add_natCast
deleted theorem Nat.ceil_add_ofNat
deleted theorem Nat.ceil_add_one
deleted theorem Nat.ceil_congr
deleted theorem Nat.ceil_eq_iff
deleted theorem Nat.ceil_eq_zero
deleted theorem Nat.ceil_int
deleted theorem Nat.ceil_intCast
deleted theorem Nat.ceil_le
deleted theorem Nat.ceil_le_ceil
deleted theorem Nat.ceil_le_floor_add_one
deleted theorem Nat.ceil_le_mul
deleted theorem Nat.ceil_le_two_mul
deleted theorem Nat.ceil_lt_add_one
deleted theorem Nat.ceil_lt_mul
deleted theorem Nat.ceil_lt_two_mul
deleted theorem Nat.ceil_mono
deleted theorem Nat.ceil_nat
deleted theorem Nat.ceil_natCast
deleted theorem Nat.ceil_ofNat
deleted theorem Nat.ceil_one
deleted theorem Nat.ceil_pos
deleted theorem Nat.ceil_zero
deleted theorem Nat.div_two_lt_floor
deleted def Nat.floor
deleted theorem Nat.floor_add_natCast
deleted theorem Nat.floor_add_ofNat
deleted theorem Nat.floor_add_one
deleted theorem Nat.floor_congr
deleted theorem Nat.floor_div_eq_div
deleted theorem Nat.floor_div_natCast
deleted theorem Nat.floor_div_ofNat
deleted theorem Nat.floor_eq_iff'
deleted theorem Nat.floor_eq_iff
deleted theorem Nat.floor_eq_on_Ico'
deleted theorem Nat.floor_eq_on_Ico
deleted theorem Nat.floor_eq_zero
deleted theorem Nat.floor_int
deleted theorem Nat.floor_le
deleted theorem Nat.floor_le_ceil
deleted theorem Nat.floor_le_floor
deleted theorem Nat.floor_le_of_le
deleted theorem Nat.floor_lt'
deleted theorem Nat.floor_lt
deleted theorem Nat.floor_lt_one
deleted theorem Nat.floor_mono
deleted theorem Nat.floor_nat
deleted theorem Nat.floor_natCast
deleted theorem Nat.floor_ofNat
deleted theorem Nat.floor_of_nonpos
deleted theorem Nat.floor_one
deleted theorem Nat.floor_pos
deleted theorem Nat.floor_sub_natCast
deleted theorem Nat.floor_sub_ofNat
deleted theorem Nat.floor_sub_one
deleted theorem Nat.floor_zero
deleted theorem Nat.gc_ceil_coe
deleted theorem Nat.le_ceil
deleted theorem Nat.le_floor
deleted theorem Nat.le_floor_iff'
deleted theorem Nat.le_floor_iff
deleted theorem Nat.le_of_ceil_le
deleted theorem Nat.lt_ceil
deleted theorem Nat.lt_floor_add_one
deleted theorem Nat.lt_of_ceil_lt
deleted theorem Nat.lt_of_floor_lt
deleted theorem Nat.lt_of_lt_floor
deleted theorem Nat.lt_succ_floor
deleted theorem Nat.map_ceil
deleted theorem Nat.map_floor
deleted theorem Nat.mul_lt_floor
deleted theorem Nat.one_le_ceil_iff
deleted theorem Nat.one_le_floor_iff
deleted theorem Nat.pos_of_floor_pos
deleted theorem Nat.preimage_Icc
deleted theorem Nat.preimage_Ici
deleted theorem Nat.preimage_Ico
deleted theorem Nat.preimage_Iic
deleted theorem Nat.preimage_Iio
deleted theorem Nat.preimage_Ioc
deleted theorem Nat.preimage_Ioi
deleted theorem Nat.preimage_Ioo
deleted theorem Nat.preimage_ceil_zero
deleted theorem Nat.preimage_floor_zero
deleted theorem Nat.sub_one_lt_floor
added theorem Nat.ceil_add_le
added theorem Nat.ceil_add_natCast
added theorem Nat.ceil_add_ofNat
added theorem Nat.ceil_add_one
added theorem Nat.ceil_congr
added theorem Nat.ceil_eq_iff
added theorem Nat.ceil_eq_zero
added theorem Nat.ceil_intCast
added theorem Nat.ceil_le_ceil
added theorem Nat.ceil_le_mul
added theorem Nat.ceil_le_two_mul
added theorem Nat.ceil_lt_add_one
added theorem Nat.ceil_lt_mul
added theorem Nat.ceil_lt_two_mul
added theorem Nat.ceil_mono
added theorem Nat.ceil_natCast
added theorem Nat.ceil_ofNat
added theorem Nat.ceil_one
added theorem Nat.ceil_zero
added theorem Nat.div_two_lt_floor
added theorem Nat.floor_add_natCast
added theorem Nat.floor_add_ofNat
added theorem Nat.floor_add_one
added theorem Nat.floor_congr
added theorem Nat.floor_div_eq_div
added theorem Nat.floor_div_natCast
added theorem Nat.floor_div_ofNat
added theorem Nat.floor_eq_iff'
added theorem Nat.floor_eq_iff
added theorem Nat.floor_eq_on_Ico'
added theorem Nat.floor_eq_on_Ico
added theorem Nat.floor_eq_zero
added theorem Nat.floor_le
added theorem Nat.floor_le_ceil
added theorem Nat.floor_le_floor
added theorem Nat.floor_le_of_le
added theorem Nat.floor_lt'
added theorem Nat.floor_lt
added theorem Nat.floor_lt_one
added theorem Nat.floor_mono
added theorem Nat.floor_natCast
added theorem Nat.floor_ofNat
added theorem Nat.floor_of_nonpos
added theorem Nat.floor_one
added theorem Nat.floor_pos
added theorem Nat.floor_sub_natCast
added theorem Nat.floor_sub_ofNat
added theorem Nat.floor_sub_one
added theorem Nat.floor_zero
added theorem Nat.le_ceil
added theorem Nat.le_floor_iff'
added theorem Nat.le_of_ceil_le
added theorem Nat.lt_floor_add_one
added theorem Nat.lt_of_ceil_lt
added theorem Nat.lt_of_floor_lt
added theorem Nat.lt_of_lt_floor
added theorem Nat.lt_succ_floor
added theorem Nat.map_ceil
added theorem Nat.map_floor
added theorem Nat.mul_lt_floor
added theorem Nat.one_le_ceil_iff
added theorem Nat.one_le_floor_iff
added theorem Nat.pos_of_floor_pos
added theorem Nat.preimage_Icc
added theorem Nat.preimage_Ici
added theorem Nat.preimage_Ico
added theorem Nat.preimage_Iic
added theorem Nat.preimage_Iio
added theorem Nat.preimage_Ioc
added theorem Nat.preimage_Ioi
added theorem Nat.preimage_Ioo
added theorem Nat.preimage_ceil_zero
added theorem Nat.sub_one_lt_floor