Commit 2023-04-11 09:57 2d0dd390

View on Github →

feat: port Algebra.Order.ToIntervalMod (#2148) Only now realized that this is part of an ongoing project within mathlib3, see https://github.com/leanprover-community/mathlib/pull/17743. Might be best to wait.

Estimated changes

added def MemIooMod
added theorem left_le_toIcoMod
added theorem left_lt_toIocMod
added theorem self_sub_toIcoMod
added theorem self_sub_toIocMod
added theorem tFAE_memIooMod
added def toIcoDiv
added theorem toIcoDiv_add_left
added theorem toIcoDiv_add_right'
added theorem toIcoDiv_add_right
added theorem toIcoDiv_add_zsmul
added theorem toIcoDiv_apply_left
added theorem toIcoDiv_apply_right
added theorem toIcoDiv_eq_floor
added theorem toIcoDiv_neg
added theorem toIcoDiv_sub'
added theorem toIcoDiv_sub
added theorem toIcoDiv_sub_zsmul
added theorem toIcoDiv_zero_one
added theorem toIcoDiv_zsmul_add
added def toIcoMod
added theorem toIcoMod_add_left
added theorem toIcoMod_add_right'
added theorem toIcoMod_add_right
added theorem toIcoMod_add_zsmul
added theorem toIcoMod_apply_left
added theorem toIcoMod_apply_right
added theorem toIcoMod_eq_fract_mul
added theorem toIcoMod_eq_iff
added theorem toIcoMod_eq_self
added theorem toIcoMod_eq_toIcoMod
added theorem toIcoMod_le_toIocMod
added theorem toIcoMod_lt_right
added theorem toIcoMod_mem_Ico'
added theorem toIcoMod_mem_Ico
added theorem toIcoMod_neg
added theorem toIcoMod_periodic
added theorem toIcoMod_sub'
added theorem toIcoMod_sub
added theorem toIcoMod_sub_self
added theorem toIcoMod_sub_zsmul
added theorem toIcoMod_toIcoMod
added theorem toIcoMod_toIocMod
added theorem toIcoMod_zero_one
added theorem toIcoMod_zsmul_add
added def toIocDiv
added theorem toIocDiv_add_left
added theorem toIocDiv_add_right'
added theorem toIocDiv_add_right
added theorem toIocDiv_add_zsmul
added theorem toIocDiv_apply_left
added theorem toIocDiv_apply_right
added theorem toIocDiv_eq_neg_floor
added theorem toIocDiv_neg
added theorem toIocDiv_sub'
added theorem toIocDiv_sub
added theorem toIocDiv_sub_zsmul
added theorem toIocDiv_zsmul_add
added def toIocMod
added theorem toIocMod_add_left
added theorem toIocMod_add_right'
added theorem toIocMod_add_right
added theorem toIocMod_add_zsmul
added theorem toIocMod_apply_left
added theorem toIocMod_apply_right
added theorem toIocMod_eq_iff
added theorem toIocMod_eq_self
added theorem toIocMod_eq_toIocMod
added theorem toIocMod_le_right
added theorem toIocMod_mem_Ioc
added theorem toIocMod_neg
added theorem toIocMod_periodic
added theorem toIocMod_sub'
added theorem toIocMod_sub
added theorem toIocMod_sub_self
added theorem toIocMod_sub_zsmul
added theorem toIocMod_toIcoMod
added theorem toIocMod_toIocMod
added theorem toIocMod_zsmul_add
added theorem unionᵢ_Icc_add_zsmul
added theorem unionᵢ_Icc_int_cast
added theorem unionᵢ_Icc_zsmul
added theorem unionᵢ_Ico_add_zsmul
added theorem unionᵢ_Ico_int_cast
added theorem unionᵢ_Ico_zsmul
added theorem unionᵢ_Ioc_add_zsmul
added theorem unionᵢ_Ioc_int_cast
added theorem unionᵢ_Ioc_zsmul