Commit 2023-01-10 17:53 3edd6391

View on Github →

feat: port Algebra.Order.Floor (#1304) This PR provided some of the first serious testing of linarith and abel, resulting in bugfixes #1358 and #1394.

depends on: #1392
depends on: #1394

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Floor.lean

added def FloorRing.ofCeil

added def FloorRing.ofFloor

added theorem Int.abs_fract

added theorem Int.abs_one_sub_fract

added theorem Int.abs_sub_lt_one_of_floor_eq_floor

added theorem Int.add_one_le_ceil_iff

added def Int.ceil

added theorem Int.ceil_add_ceil_le

added theorem Int.ceil_add_int

added theorem Int.ceil_add_le

added theorem Int.ceil_add_nat

added theorem Int.ceil_add_one

added theorem Int.ceil_congr

added theorem Int.ceil_eq_add_one_sub_fract

added theorem Int.ceil_eq_iff

added theorem Int.ceil_eq_on_Ioc'

added theorem Int.ceil_eq_on_Ioc

added theorem Int.ceil_eq_zero_iff

added theorem Int.ceil_int

added theorem Int.ceil_intCast

added theorem Int.ceil_le

added theorem Int.ceil_le_floor_add_one

added theorem Int.ceil_lt_add_one

added theorem Int.ceil_mono

added theorem Int.ceil_natCast

added theorem Int.ceil_neg

added theorem Int.ceil_nonneg

added theorem Int.ceil_one

added theorem Int.ceil_pos

added theorem Int.ceil_sub_int

added theorem Int.ceil_sub_nat

added theorem Int.ceil_sub_one

added theorem Int.ceil_sub_self_eq

added theorem Int.ceil_toNat

added theorem Int.ceil_zero

added def Int.floor

added theorem Int.floorRing_ceil_eq

added theorem Int.floorRing_floor_eq

added theorem Int.floor_add_fract

added theorem Int.floor_add_int

added theorem Int.floor_add_nat

added theorem Int.floor_add_one

added theorem Int.floor_congr

added theorem Int.floor_eq_iff

added theorem Int.floor_eq_on_Ico'

added theorem Int.floor_eq_on_Ico

added theorem Int.floor_eq_zero_iff

added theorem Int.floor_fract

added theorem Int.floor_int

added theorem Int.floor_intCast

added theorem Int.floor_int_add

added theorem Int.floor_le

added theorem Int.floor_le_ceil

added theorem Int.floor_le_neg_one_iff

added theorem Int.floor_le_sub_one_iff

added theorem Int.floor_lt

added theorem Int.floor_lt_ceil_of_lt

added theorem Int.floor_mono

added theorem Int.floor_natCast

added theorem Int.floor_nat_add

added theorem Int.floor_neg

added theorem Int.floor_nonneg

added theorem Int.floor_nonpos

added theorem Int.floor_one

added theorem Int.floor_pos

added theorem Int.floor_sub_int

added theorem Int.floor_sub_nat

added theorem Int.floor_toNat

added theorem Int.floor_zero

added def Int.fract

added theorem Int.fract_add

added theorem Int.fract_add_floor

added theorem Int.fract_add_fract_le

added theorem Int.fract_add_int

added theorem Int.fract_add_le

added theorem Int.fract_add_nat

added theorem Int.fract_div_intCast_eq_div_intCast_mod

added theorem Int.fract_div_mul_self_add_zsmul_eq

added theorem Int.fract_div_mul_self_mem_Ico

added theorem Int.fract_div_natCast_eq_div_natCast_mod

added theorem Int.fract_eq_fract

added theorem Int.fract_eq_iff

added theorem Int.fract_eq_self

added theorem Int.fract_eq_zero_or_add_one_sub_ceil

added theorem Int.fract_floor

added theorem Int.fract_fract

added theorem Int.fract_int

added theorem Int.fract_intCast

added theorem Int.fract_int_add

added theorem Int.fract_int_nat

added theorem Int.fract_lt_one

added theorem Int.fract_mul_nat

added theorem Int.fract_natCast

added theorem Int.fract_neg

added theorem Int.fract_neg_eq_zero

added theorem Int.fract_nonneg

added theorem Int.fract_one

added theorem Int.fract_sub_int

added theorem Int.fract_sub_nat

added theorem Int.fract_sub_self

added theorem Int.fract_zero

added theorem Int.gc_ceil_coe

added theorem Int.gc_coe_floor

added theorem Int.image_fract

added theorem Int.le_ceil

added theorem Int.le_floor

added theorem Int.le_floor_add

added theorem Int.le_floor_add_floor

added theorem Int.lt_ceil

added theorem Int.lt_floor_add_one

added theorem Int.lt_succ_floor

added theorem Int.map_ceil

added theorem Int.map_floor

added theorem Int.map_fract

added theorem Int.map_round

added theorem Int.one_le_ceil_iff

added theorem Int.preimage_Icc

added theorem Int.preimage_Ici

added theorem Int.preimage_Ico

added theorem Int.preimage_Iic

added theorem Int.preimage_Iio

added theorem Int.preimage_Ioc

added theorem Int.preimage_Ioi

added theorem Int.preimage_Ioo

added theorem Int.preimage_ceil_singleton

added theorem Int.preimage_floor_singleton

added theorem Int.preimage_fract

added theorem Int.self_sub_floor

added theorem Int.self_sub_fract

added theorem Int.sub_floor_div_mul_lt

added theorem Int.sub_floor_div_mul_nonneg

added theorem Int.sub_one_lt_floor

added theorem Nat.add_one_le_ceil_iff

added theorem Nat.cast_ceil_eq_cast_int_ceil

added theorem Nat.cast_ceil_eq_int_ceil

added theorem Nat.cast_floor_eq_cast_int_floor

added theorem Nat.cast_floor_eq_int_floor

added def Nat.ceil

added theorem Nat.ceil_add_le

added theorem Nat.ceil_add_nat

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_int

added theorem Nat.ceil_intCast

added theorem Nat.ceil_le

added theorem Nat.ceil_le_floor_add_one

added theorem Nat.ceil_lt_add_one

added theorem Nat.ceil_mono

added theorem Nat.ceil_nat

added theorem Nat.ceil_natCast

added theorem Nat.ceil_one

added theorem Nat.ceil_pos

added theorem Nat.ceil_zero

added def Nat.floor

added theorem Nat.floor_add_nat

added theorem Nat.floor_add_one

added theorem Nat.floor_coe

added theorem Nat.floor_congr

added theorem Nat.floor_div_eq_div

added theorem Nat.floor_div_nat

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_int

added theorem Nat.floor_le

added theorem Nat.floor_le_ceil

added theorem Nat.floor_le_of_le

added theorem Nat.floor_le_one_of_le_one

added theorem Nat.floor_lt'

added theorem Nat.floor_lt

added theorem Nat.floor_lt_ceil_of_lt_of_pos

added theorem Nat.floor_lt_one

added theorem Nat.floor_mono

added theorem Nat.floor_nat

added theorem Nat.floor_of_nonpos

added theorem Nat.floor_one

added theorem Nat.floor_pos

added theorem Nat.floor_sub_nat

added theorem Nat.floor_zero

added theorem Nat.gc_ceil_coe

added theorem Nat.le_ceil

added theorem Nat.le_floor

added theorem Nat.le_floor_iff'

added theorem Nat.le_floor_iff

added theorem Nat.le_of_ceil_le

added theorem Nat.lt_ceil

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_one_of_floor_lt_one

added theorem Nat.lt_succ_floor

added theorem Nat.map_ceil

added theorem Nat.map_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_of_ne_zero

added theorem Nat.preimage_ceil_zero

added theorem Nat.preimage_floor_of_ne_zero

added theorem Nat.preimage_floor_zero

added theorem Nat.sub_one_lt_floor

added theorem abs_sub_round

added theorem abs_sub_round_div_natCast_eq

added theorem abs_sub_round_eq_min

added def round

added theorem round_add_int

added theorem round_add_nat

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_natCast

added theorem round_nat_add

added theorem round_neg_two_inv

added theorem round_one

added theorem round_sub_int

added theorem round_sub_nat

added theorem round_sub_one

added theorem round_two_inv

added theorem round_zero

added theorem subsingleton_floorRing

added theorem subsingleton_floorSemiring

Modified Mathlib/Data/Int/Cast/Basic.lean

Modified Mathlib/Init/Meta/WellFoundedTactics.lean