Commit 2023-05-13 08:55 a39c3143

View on Github →

feat: port Algebra.Order.ToIntervalMod (#3952)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/ToIntervalMod.lean

added theorem AddCommGroup.modEq_iff_not_forall_mem_Ioo_mod

added theorem AddCommGroup.modEq_iff_toIcoDiv_eq_toIocDiv_add_one

added theorem AddCommGroup.modEq_iff_toIcoMod_add_period_eq_toIocMod

added theorem AddCommGroup.modEq_iff_toIcoMod_eq_left

added theorem AddCommGroup.modEq_iff_toIcoMod_ne_toIocMod

added theorem AddCommGroup.modEq_iff_toIocMod_eq_right

added theorem AddCommGroup.not_modEq_iff_toIcoDiv_eq_toIocDiv

added theorem AddCommGroup.not_modEq_iff_toIcoMod_eq_toIocMod

added theorem AddCommGroup.tfae_modEq

added theorem Ico_eq_locus_Ioc_eq_unionᵢ_Ioo

added theorem left_le_toIcoMod

added theorem left_lt_toIocMod

added theorem quotientAddGroup.btw_coe_iff'

added theorem quotientAddGroup.btw_coe_iff

added def quotientAddGroup.equivIcoMod

added theorem quotientAddGroup.equivIcoMod_coe

added theorem quotientAddGroup.equivIcoMod_zero

added def quotientAddGroup.equivIocMod

added theorem quotientAddGroup.equivIocMod_coe

added theorem quotientAddGroup.equivIocMod_zero

added theorem self_sub_toIcoDiv_zsmul

added theorem self_sub_toIcoMod

added theorem self_sub_toIocDiv_zsmul

added theorem self_sub_toIocMod

added theorem sub_toIcoDiv_zsmul_mem_Ico

added theorem sub_toIocDiv_zsmul_mem_Ioc

added def toIcoDiv

added theorem toIcoDiv_add_left'

added theorem toIcoDiv_add_left

added theorem toIcoDiv_add_right'

added theorem toIcoDiv_add_right

added theorem toIcoDiv_add_zsmul'

added theorem toIcoDiv_add_zsmul

added theorem toIcoDiv_apply_left

added theorem toIcoDiv_apply_right

added theorem toIcoDiv_eq_floor

added theorem toIcoDiv_eq_of_sub_zsmul_mem_Ico

added theorem toIcoDiv_eq_sub

added theorem toIcoDiv_neg'

added theorem toIcoDiv_neg

added theorem toIcoDiv_sub'

added theorem toIcoDiv_sub

added theorem toIcoDiv_sub_eq_toIcoDiv_add'

added theorem toIcoDiv_sub_eq_toIcoDiv_add

added theorem toIcoDiv_sub_zsmul'

added theorem toIcoDiv_sub_zsmul

added theorem toIcoDiv_zero_one

added theorem toIcoDiv_zsmul_add

added theorem toIcoDiv_zsmul_sub_self

added theorem toIcoDiv_zsmul_sub_toIcoMod

added def toIcoMod

added theorem toIcoMod_add_left'

added theorem toIcoMod_add_left

added theorem toIcoMod_add_right'

added theorem toIcoMod_add_right

added theorem toIcoMod_add_right_eq_add

added theorem toIcoMod_add_toIcoDiv_zsmul

added theorem toIcoMod_add_toIocMod_zero

added theorem toIcoMod_add_zsmul'

added theorem toIcoMod_add_zsmul

added theorem toIcoMod_apply_left

added theorem toIcoMod_apply_right

added theorem toIcoMod_eq_add_fract_mul

added theorem toIcoMod_eq_fract_mul

added theorem toIcoMod_eq_iff

added theorem toIcoMod_eq_self

added theorem toIcoMod_eq_sub

added theorem toIcoMod_eq_toIcoMod

added theorem toIcoMod_inj

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_neg

added theorem toIcoMod_periodic

added theorem toIcoMod_sub'

added theorem toIcoMod_sub

added theorem toIcoMod_sub_eq_sub

added theorem toIcoMod_sub_self

added theorem toIcoMod_sub_zsmul'

added theorem toIcoMod_sub_zsmul

added theorem toIcoMod_toIcoMod

added theorem toIcoMod_toIocMod

added theorem toIcoMod_zero_one

added theorem toIcoMod_zero_sub_comm

added theorem toIcoMod_zsmul_add'

added theorem toIcoMod_zsmul_add

added def toIocDiv

added theorem toIocDiv_add_left'

added theorem toIocDiv_add_left

added theorem toIocDiv_add_right'

added theorem toIocDiv_add_right

added theorem toIocDiv_add_zsmul'

added theorem toIocDiv_add_zsmul

added theorem toIocDiv_apply_left

added theorem toIocDiv_apply_right

added theorem toIocDiv_eq_neg_floor

added theorem toIocDiv_eq_of_sub_zsmul_mem_Ioc

added theorem toIocDiv_eq_sub

added theorem toIocDiv_neg'

added theorem toIocDiv_neg

added theorem toIocDiv_sub'

added theorem toIocDiv_sub

added theorem toIocDiv_sub_eq_toIocDiv_add'

added theorem toIocDiv_sub_eq_toIocDiv_add

added theorem toIocDiv_sub_zsmul'

added theorem toIocDiv_sub_zsmul

added theorem toIocDiv_wcovby_toIcoDiv

added theorem toIocDiv_zsmul_add

added theorem toIocDiv_zsmul_sub_self

added theorem toIocDiv_zsmul_sub_toIocMod

added def toIocMod

added theorem toIocMod_add_left'

added theorem toIocMod_add_left

added theorem toIocMod_add_right'

added theorem toIocMod_add_right

added theorem toIocMod_add_right_eq_add

added theorem toIocMod_add_toIcoMod_zero

added theorem toIocMod_add_toIocDiv_zsmul

added theorem toIocMod_add_zsmul'

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_sub

added theorem toIocMod_eq_sub_fract_mul

added theorem toIocMod_eq_toIocMod

added theorem toIocMod_le_right

added theorem toIocMod_le_toIcoMod_add

added theorem toIocMod_mem_Ioc

added theorem toIocMod_neg'

added theorem toIocMod_neg

added theorem toIocMod_periodic

added theorem toIocMod_sub'

added theorem toIocMod_sub

added theorem toIocMod_sub_eq_sub

added theorem toIocMod_sub_self

added theorem toIocMod_sub_zsmul'

added theorem toIocMod_sub_zsmul

added theorem toIocMod_toIcoMod

added theorem toIocMod_toIocMod

added theorem toIocMod_zero_sub_comm

added theorem toIocMod_zsmul_add'

added theorem toIocMod_zsmul_add

added theorem unionᵢ_Icc_add_int_cast

added theorem unionᵢ_Icc_add_zsmul

added theorem unionᵢ_Icc_int_cast

added theorem unionᵢ_Icc_zsmul

added theorem unionᵢ_Ico_add_int_cast

added theorem unionᵢ_Ico_add_zsmul

added theorem unionᵢ_Ico_int_cast

added theorem unionᵢ_Ico_zsmul

added theorem unionᵢ_Ioc_add_int_cast

added theorem unionᵢ_Ioc_add_zsmul

added theorem unionᵢ_Ioc_int_cast

added theorem unionᵢ_Ioc_zsmul