Commit 2023-05-16 06:36 a183081f

View on Github →

feat: port Topology.Instances.AddCircle (#3984)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/CharZero/Quotient.lean

added theorem QuotientAddGroup.zmultiples_nsmul_eq_nsmul_iff

added theorem QuotientAddGroup.zmultiples_zsmul_eq_zsmul_iff

deleted theorem quotientAddGroup.zmultiples_nsmul_eq_nsmul_iff

deleted theorem quotientAddGroup.zmultiples_zsmul_eq_zsmul_iff

Modified Mathlib/Algebra/Order/ToIntervalMod.lean

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

deleted theorem quotientAddGroup.btw_coe_iff'

deleted theorem quotientAddGroup.btw_coe_iff

deleted def quotientAddGroup.equivIcoMod

deleted theorem quotientAddGroup.equivIcoMod_coe

deleted theorem quotientAddGroup.equivIcoMod_zero

deleted def quotientAddGroup.equivIocMod

deleted theorem quotientAddGroup.equivIocMod_coe

deleted theorem quotientAddGroup.equivIocMod_zero

Created Mathlib/Topology/Instances/AddCircle.lean

added inductive AddCircle.EndpointIdent

added theorem AddCircle.addOrderOf_coe_rat

added theorem AddCircle.addOrderOf_div_of_gcd_eq_one'

added theorem AddCircle.addOrderOf_div_of_gcd_eq_one

added theorem AddCircle.addOrderOf_eq_pos_iff

added theorem AddCircle.addOrderOf_period_div

added theorem AddCircle.card_addOrderOf_eq_totient

added theorem AddCircle.coe_add

added theorem AddCircle.coe_add_period

added theorem AddCircle.coe_eq_coe_iff_of_mem_Ico

added theorem AddCircle.coe_eq_zero_iff

added theorem AddCircle.coe_eq_zero_of_pos_iff

added theorem AddCircle.coe_equivIco_mk_apply

added theorem AddCircle.coe_image_Icc_eq

added theorem AddCircle.coe_image_Ico_eq

added theorem AddCircle.coe_image_Ioc_eq

added theorem AddCircle.coe_neg

added theorem AddCircle.coe_nsmul

added theorem AddCircle.coe_period

added theorem AddCircle.coe_sub

added theorem AddCircle.coe_zsmul

added theorem AddCircle.continuousAt_equivIco

added theorem AddCircle.continuousAt_equivIoc

added theorem AddCircle.continuous_equivIco_symm

added theorem AddCircle.continuous_equivIoc_symm

added def AddCircle.equivAddCircle

added theorem AddCircle.equivAddCircle_apply_mk

added theorem AddCircle.equivAddCircle_symm_apply_mk

added def AddCircle.equivIccQuot

added theorem AddCircle.equivIccQuot_comp_mk_eq_toIcoMod

added theorem AddCircle.equivIccQuot_comp_mk_eq_toIocMod

added def AddCircle.equivIco

added def AddCircle.equivIoc

added theorem AddCircle.exists_gcd_eq_one_of_isOfFinAddOrder

added theorem AddCircle.finite_setOf_add_order_eq

added theorem AddCircle.gcd_mul_addOrderOf_div_eq

added def AddCircle.homeoIccQuot

added def AddCircle.liftIco

added theorem AddCircle.liftIco_coe_apply

added theorem AddCircle.liftIco_continuous

added theorem AddCircle.liftIco_eq_lift_Icc

added theorem AddCircle.liftIco_zero_coe_apply

added theorem AddCircle.liftIco_zero_continuous

added def AddCircle.liftIoc

added theorem AddCircle.liftIoc_coe_apply

added def AddCircle.setAddOrderOfEquiv

added def AddCircle

added theorem continuousAt_toIcoMod

added theorem continuousAt_toIocMod

added theorem continuous_left_toIocMod

added theorem continuous_right_toIcoMod

added theorem toIcoMod_eventuallyEq_toIocMod