Defs

📁 Source: Mathlib/Topology/Instances/AddCircle/Defs.lean

Statistics

Metric	Count
Definitions EndpointIdent, equivAddCircle, equivIccQuot, equivIco, equivIoc, homeoIccQuot, homeomorphAddCircle, instDivisibleByInt, liftIco, liftIoc, openPartialHomeomorphCoe, partialHomeomorphCoe, setAddOrderOfEquiv	13
Theorems Ico_ext, Ioc_ext, addOrderOf_coe_rat, addOrderOf_div_of_gcd_eq_one, addOrderOf_div_of_gcd_eq_one', addOrderOf_eq_pos_iff, addOrderOf_period_div, card_addOrderOf_eq_totient, card_torsion_le_of_isSMulRegular, card_torsion_le_of_isSMulRegular_int, coe_add, coe_add_period, coe_eq_coe_iff_of_mem_Ico, coe_eq_zero_iff, coe_eq_zero_iff_of_mem_Ico, coe_eq_zero_of_pos_iff, coe_equivIco_mk_apply, coe_fract, coe_image_Icc_eq, coe_image_Ico_eq, coe_image_Ioc_eq, coe_neg, coe_nsmul, coe_period, coe_sub, coe_zero, coe_zsmul, continuousAt_equivIco, continuousAt_equivIoc, continuous_equivIco_symm, continuous_equivIoc_symm, continuous_mk', eq_coe_Ico, equivAddCircle_apply_mk, equivAddCircle_symm_apply_mk, equivIccQuot_comp_mk_eq_toIcoMod, equivIccQuot_comp_mk_eq_toIocMod, equivIco_coe_eq, equivIoc_coe_eq, exists_gcd_eq_one_of_isOfFinAddOrder, finite_setOf_addOrderOf_eq, finite_torsion, finite_torsion_of_isSMulRegular, finite_torsion_of_isSMulRegular_int, gcd_mul_addOrderOf_div_eq, homeomorphAddCircle_apply_mk, homeomorphAddCircle_symm_apply_mk, intCast_div_mul_eq_zsmul, isOfFinAddOrder_iff_exists_rat_eq_div, liftIco_coe_apply, liftIco_comp_apply, liftIco_continuous, liftIco_eq_lift_Icc, liftIco_zero_coe_apply, liftIco_zero_continuous, liftIoc_coe_apply, liftIoc_comp_apply, liftIoc_continuous, liftIoc_eq_liftIco, liftIoc_eq_lift_Icc, liftIoc_zero_coe_apply, liftIoc_zero_continuous, natCast_div_mul_eq_nsmul, not_isOfFinAddOrder_iff_forall_rat_ne_div, nsmul_eq_zero_iff, openPartialHomeomorphCoe_apply, openPartialHomeomorphCoe_source, openPartialHomeomorphCoe_symm_apply, openPartialHomeomorphCoe_target, continuousAt_toIcoDiv, continuousAt_toIcoMod, continuousAt_toIocDiv, continuousAt_toIocMod, continuousOn_toIcoDiv, continuousOn_toIocDiv, continuousWithinAt_toIcoDiv_Ici, continuousWithinAt_toIcoMod_Ici, continuousWithinAt_toIocDiv_Iic, continuousWithinAt_toIocMod_Iic, continuous_left_toIocMod, continuous_right_toIcoMod, eventuallyEq_toIcoDiv_nhds, eventuallyEq_toIcoDiv_nhdsGE, eventuallyEq_toIcoDiv_nhdsLT, eventuallyEq_toIocDiv_nhds, eventuallyEq_toIocDiv_nhdsGT, eventuallyEq_toIocDiv_nhdsLE, toIcoMod_eventuallyEq_toIocMod	88
Total	101

AddCircle

Definitions

Name	Category	Theorems
EndpointIdent 📖	CompData	4 math math: equivIccQuot_comp_mk_eq_toIcoMod, equivIccQuot_comp_mk_eq_toIocMod, liftIoc_eq_lift_Icc, liftIco_eq_lift_Icc
equivAddCircle 📖	CompOp	2 math math: equivAddCircle_apply_mk, equivAddCircle_symm_apply_mk
equivIccQuot 📖	CompOp	4 math math: equivIccQuot_comp_mk_eq_toIcoMod, equivIccQuot_comp_mk_eq_toIocMod, liftIoc_eq_lift_Icc, liftIco_eq_lift_Icc
equivIco 📖	CompOp	5 math math: coe_equivIco_mk_apply, equivIco_coe_eq, continuous_equivIco_symm, continuousAt_equivIco, openPartialHomeomorphCoe_symm_apply
equivIoc 📖	CompOp	4 math math: continuous_equivIoc_symm, measurePreserving_equivIoc, equivIoc_coe_eq, continuousAt_equivIoc
homeoIccQuot 📖	CompOp	—
homeomorphAddCircle 📖	CompOp	2 math math: homeomorphAddCircle_apply_mk, homeomorphAddCircle_symm_apply_mk
instDivisibleByInt 📖	CompOp	—
liftIco 📖	CompOp	8 math math: liftIco_continuous, liftIco_comp_apply, liftIco_zero_coe_apply, liftIoc_eq_liftIco, liftIco_zero_continuous, liftIco_coe_apply, liftIco_eq_lift_Icc, fourierCoeff_liftIco_eq
liftIoc 📖	CompOp	10 math math: liftIoc_zero_continuous, MeasureTheory.MemLp.memLp_liftIoc, liftIoc_comp_apply, liftIoc_zero_coe_apply, liftIoc_coe_apply, liftIoc_eq_liftIco, liftIoc_eq_lift_Icc, liftIoc_continuous, integral_liftIoc_eq_intervalIntegral, fourierCoeff_liftIoc_eq
openPartialHomeomorphCoe 📖	CompOp	4 math math: openPartialHomeomorphCoe_source, openPartialHomeomorphCoe_symm_apply, openPartialHomeomorphCoe_apply, openPartialHomeomorphCoe_target
partialHomeomorphCoe 📖	CompOp	—
setAddOrderOfEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Ico_ext 📖	—	AddCommGroup.toAddGroup AddSubgroup.zmultiples	—	—	Set.eqOn_univ coe_image_Ico_eq
Ioc_ext 📖	—	AddCommGroup.toAddGroup AddSubgroup.zmultiples	—	—	Set.eqOn_univ coe_image_Ioc_eq
addOrderOf_coe_rat 📖	mathematical	—	addOrderOf HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing QuotientAddGroup.instHasQuotientAddSubgroup AddSubgroup.zmultiples SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivisionRing.toRatCast	—	Nat.cast_zero Int.cast_zero IsStrictOrderedRing.toCharZero Int.instCharZero LT.lt.ne Rat.pos AddSubgroup.normal_of_comm Rat.cast_divInt_of_ne_zero Int.cast_natCast addOrderOf_div_of_gcd_eq_one'
addOrderOf_div_of_gcd_eq_one 📖	mathematical	—	addOrderOf HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing QuotientAddGroup.instHasQuotientAddSubgroup AddSubgroup.zmultiples SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	AddSubgroup.normal_of_comm one_mul gcd_mul_addOrderOf_div_eq
addOrderOf_div_of_gcd_eq_one' 📖	mathematical	—	addOrderOf HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing QuotientAddGroup.instHasQuotientAddSubgroup AddSubgroup.zmultiples SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddGroupWithOne.toIntCast Ring.toAddGroupWithOne AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne	—	AddSubgroup.normal_of_comm Int.cast_natCast addOrderOf_div_of_gcd_eq_one Int.cast_negSucc neg_div neg_mul addOrderOf_neg
addOrderOf_eq_pos_iff 📖	mathematical	—	addOrderOf AddCircle Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddCommGroup.toAddGroup AddSubgroup.zmultiples AddSubgroup.normal_of_comm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	AddSubgroup.normal_of_comm QuotientAddGroup.induction_on nsmul_eq_zero_iff addOrderOf_nsmul_eq_zero mul_right_cancel₀ IsCancelMulZero.toIsRightCancelMulZero Nat.instIsCancelMulZero LT.lt.ne' one_mul gcd_mul_addOrderOf_div_eq addOrderOf_div_of_gcd_eq_one
addOrderOf_period_div 📖	mathematical	—	addOrderOf HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing QuotientAddGroup.instHasQuotientAddSubgroup AddSubgroup.zmultiples SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	AddSubgroup.normal_of_comm addOrderOf_eq_iff Nat.cast_pos IsStrictOrderedRing.toIsOrderedRing DivisionRing.toNontrivial nsmul_eq_mul mul_div_cancel₀ LT.lt.ne' coe_period coe_eq_zero_of_pos_iff IsOrderedRing.toIsOrderedAddMonoid Fact.out mul_pos IsStrictOrderedRing.toPosMulStrictMono div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LE.le.not_gt mul_comm IsStrictOrderedRing.toCharZero mul_left_injective₀ IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Field.isDomain Nat.cast_mul mul_right_comm eq_div_iff mul_div
card_addOrderOf_eq_totient 📖	mathematical	—	Nat.card AddCircle Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddCommGroup.toAddGroup AddSubgroup.zmultiples AddSubgroup.normal_of_comm Nat.totient	—	AddSubgroup.normal_of_comm em Set.coe_setOf Set.infinite_coe_iff infinite_not_isOfFinAddOrder Nat.card_eq_zero_of_infinite Nat.card_of_isEmpty Nat.card_congr Nat.totient_eq_card_lt_and_coprime
card_torsion_le_of_isSMulRegular 📖	mathematical	IsSMulRegular AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	ENat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Set.encard AddCircle setOf QuotientAddGroup.Quotient.addGroup AddSubgroup.zmultiples AddSubgroup.normal_of_comm NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup ENat.instNatCast	—	AddSubgroup.normal_of_comm QuotientAddGroup.mk_surjective QuotientAddGroup.eq_zero_iff QuotientAddGroup.mk_nsmul Set.mem_setOf coe_period smul_zero smul_sub sub_eq_iff_eq_add Int.divModEquiv_symm_apply Equiv.symm_apply_apply add_comm mul_comm add_smul natCast_zsmul SemigroupAction.mul_smul LE.le.trans ENat.card_le_card_of_injective ENat.card_eq_coe_fintype_card Fintype.card_fin
card_torsion_le_of_isSMulRegular_int 📖	mathematical	IsSMulRegular SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	ENat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Set.encard AddCircle setOf QuotientAddGroup.Quotient.addGroup AddSubgroup.zmultiples AddSubgroup.normal_of_comm NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup ENat.instNatCast	—	AddSubgroup.normal_of_comm card_torsion_le_of_isSMulRegular IsSMulRegular.natAbs_iff
coe_add 📖	mathematical	—	AddCommGroup.toAddGroup AddSubgroup.zmultiples AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup QuotientAddGroup.Quotient.addCommGroup	—	—
coe_add_period 📖	mathematical	—	AddCommGroup.toAddGroup AddSubgroup.zmultiples AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	coe_add eq_sub_iff_add_eq' AddSubgroup.normal_of_comm sub_self coe_period
coe_eq_coe_iff_of_mem_Ico 📖	mathematical	Set Set.instMembership Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	AddCommGroup.toAddGroup AddSubgroup.zmultiples	—	Equiv.right_inv
coe_eq_zero_iff 📖	mathematical	—	AddCommGroup.toAddGroup AddSubgroup.zmultiples HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup SubNegMonoid.toZSMul AddGroup.toSubNegMonoid	—	AddSubgroup.normal_of_comm
coe_eq_zero_iff_of_mem_Ico 📖	mathematical	Set Set.instMembership Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	AddCommGroup.toAddGroup AddSubgroup.zmultiples HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup QuotientAddGroup.Quotient.addCommGroup	—	zero_add Fact.out coe_eq_coe_iff_of_mem_Ico AddSubgroup.normal_of_comm QuotientAddGroup.mk_zero
coe_eq_zero_of_pos_iff 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	AddCommGroup.toAddGroup AddSubgroup.zmultiples HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup QuotientAddGroup.Quotient.addCommGroup AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	coe_eq_zero_iff Mathlib.Tactic.Contrapose.contrapose₁ IsOrderedAddMonoid.toAddLeftMono zsmul_neg' zsmul_nonneg LT.lt.le neg_nonneg Int.instAddLeftMono natCast_zsmul
coe_equivIco_mk_apply 📖	mathematical	—	Set Set.instMembership Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing DFunLike.coe Equiv AddCircle Set.Elem EquivLike.toFunLike Equiv.instEquivLike equivIco IsOrderedRing.toIsOrderedAddMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsStrictOrderedRing.toIsOrderedRing FloorRing.archimedean AddCommGroup.toAddGroup AddSubgroup.zmultiples Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Int.fract DivInvMonoid.toDiv DivisionRing.toDivInvMonoid	—	toIcoMod_eq_fract_mul
coe_fract 📖	mathematical	—	AddCommGroup.toAddGroup Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing AddSubgroup.zmultiples AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.fract	—	AddSubgroup.normal_of_comm zsmul_eq_mul mul_one
coe_image_Icc_eq 📖	mathematical	—	Set.image HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup QuotientAddGroup.instHasQuotientAddSubgroup AddSubgroup.zmultiples Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid Set.univ	—	eq_top_mono Set.image_mono Set.Ico_subset_Icc_self coe_image_Ico_eq
coe_image_Ico_eq 📖	mathematical	—	Set.image HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup QuotientAddGroup.instHasQuotientAddSubgroup AddSubgroup.zmultiples Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid Set.univ	—	Set.image_eq_range Equiv.range_eq_univ
coe_image_Ioc_eq 📖	mathematical	—	Set.image HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup QuotientAddGroup.instHasQuotientAddSubgroup AddSubgroup.zmultiples Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid Set.univ	—	Set.image_eq_range Equiv.range_eq_univ
coe_neg 📖	mathematical	—	AddCommGroup.toAddGroup AddSubgroup.zmultiples NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup QuotientAddGroup.Quotient.addCommGroup	—	—
coe_nsmul 📖	mathematical	—	AddCommGroup.toAddGroup AddSubgroup.zmultiples AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm	—	—
coe_period 📖	mathematical	—	AddCommGroup.toAddGroup AddSubgroup.zmultiples HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup	—	AddSubgroup.normal_of_comm QuotientAddGroup.eq_zero_iff AddSubgroup.mem_zmultiples
coe_sub 📖	mathematical	—	AddCommGroup.toAddGroup AddSubgroup.zmultiples SubNegMonoid.toSub AddGroup.toSubNegMonoid HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm	—	—
coe_zero 📖	mathematical	—	AddCommGroup.toAddGroup AddSubgroup.zmultiples NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddCircle QuotientAddGroup.Quotient.addCommGroup	—	—
coe_zsmul 📖	mathematical	—	AddCommGroup.toAddGroup AddSubgroup.zmultiples SubNegMonoid.toZSMul AddGroup.toSubNegMonoid HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm	—	—
continuousAt_equivIco 📖	mathematical	—	ContinuousAt AddCircle Set.Elem Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples instTopologicalSpaceSubtype Set Set.instMembership DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike equivIco	—	QuotientAddGroup.induction_on ContinuousAt.eq_1 Filter.Tendsto.eq_1 QuotientAddGroup.nhds_eq IsTopologicalAddGroup.toContinuousAdd LinearOrderedAddCommGroup.toIsTopologicalAddGroup Filter.map_map ContinuousAt.codRestrict Fact.out continuousAt_toIcoMod AddCommGroup.not_modEq_iff_ne_mod_zmultiples
continuousAt_equivIoc 📖	mathematical	—	ContinuousAt AddCircle Set.Elem Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples instTopologicalSpaceSubtype Set Set.instMembership DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike equivIoc	—	QuotientAddGroup.induction_on ContinuousAt.eq_1 Filter.Tendsto.eq_1 QuotientAddGroup.nhds_eq IsTopologicalAddGroup.toContinuousAdd LinearOrderedAddCommGroup.toIsTopologicalAddGroup Filter.map_map ContinuousAt.codRestrict Fact.out continuousAt_toIocMod AddCommGroup.not_modEq_iff_ne_mod_zmultiples
continuous_equivIco_symm 📖	mathematical	—	Continuous Set.Elem Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid AddCircle instTopologicalSpaceSubtype Set Set.instMembership QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivIco	—	Continuous.comp continuous_quotient_mk' continuous_subtype_val
continuous_equivIoc_symm 📖	mathematical	—	Continuous Set.Elem Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid AddCircle instTopologicalSpaceSubtype Set Set.instMembership QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivIoc	—	Continuous.comp continuous_quotient_mk' continuous_subtype_val
continuous_mk' 📖	mathematical	—	Continuous HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup QuotientAddGroup.instHasQuotientAddSubgroup AddSubgroup.zmultiples QuotientAddGroup.instTopologicalSpace DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm AddMonoidHom.instFunLike QuotientAddGroup.mk'	—	continuous_coinduced_rng AddSubgroup.normal_of_comm
eq_coe_Ico 📖	mathematical	—	Set Set.instMembership Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddCommGroup.toAddGroup AddSubgroup.zmultiples	—	Fact.out zero_add Equiv.symm_apply_apply
equivAddCircle_apply_mk 📖	mathematical	—	DFunLike.coe AddEquiv AddCircle Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid QuotientAddGroup.Quotient.addCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup EquivLike.toFunLike AddEquiv.instEquivLike equivAddCircle Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield	—	—
equivAddCircle_symm_apply_mk 📖	mathematical	—	DFunLike.coe AddEquiv AddCircle Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid QuotientAddGroup.Quotient.addCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm equivAddCircle Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield	—	—
equivIccQuot_comp_mk_eq_toIcoMod 📖	mathematical	—	AddCircle Set.Elem Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid EndpointIdent DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike equivIccQuot Quotient.mk'' QuotientAddGroup.leftRel AddCommGroup.toAddGroup AddSubgroup.zmultiples Set Set.instMembership toIcoMod Fact.out Preorder.toLT NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set.Ico_subset_Icc_self toIcoMod_mem_Ico	—	—
equivIccQuot_comp_mk_eq_toIocMod 📖	mathematical	—	AddCircle Set.Elem Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid EndpointIdent DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike equivIccQuot Quotient.mk'' QuotientAddGroup.leftRel AddCommGroup.toAddGroup AddSubgroup.zmultiples Set Set.instMembership toIocMod Fact.out Preorder.toLT NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set.Ioc_subset_Icc_self toIocMod_mem_Ioc	—	Fact.out Set.Ioc_subset_Icc_self toIocMod_mem_Ioc Set.Ico_subset_Icc_self toIcoMod_mem_Ico equivIccQuot_comp_mk_eq_toIcoMod AddCommGroup.modEq_iff_toIcoMod_eq_left AddCommGroup.modEq_iff_toIocMod_eq_right AddCommGroup.not_modEq_iff_toIcoMod_eq_toIocMod
equivIco_coe_eq 📖	mathematical	Set Set.instMembership Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	DFunLike.coe Equiv AddCircle Set.Elem EquivLike.toFunLike Equiv.instEquivLike equivIco AddCommGroup.toAddGroup AddSubgroup.zmultiples	—	Equiv.apply_eq_iff_eq_symm_apply equivIco.eq_1 QuotientAddGroup.equivIcoMod_symm_apply
equivIoc_coe_eq 📖	mathematical	Set Set.instMembership Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	DFunLike.coe Equiv AddCircle Set.Elem EquivLike.toFunLike Equiv.instEquivLike equivIoc AddCommGroup.toAddGroup AddSubgroup.zmultiples	—	Equiv.apply_eq_iff_eq_symm_apply equivIoc.eq_1 QuotientAddGroup.equivIocMod_symm_apply
exists_gcd_eq_one_of_isOfFinAddOrder 📖	mathematical	IsOfFinAddOrder AddCircle Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddCommGroup.toAddGroup AddSubgroup.zmultiples AddSubgroup.normal_of_comm	addOrderOf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	AddSubgroup.normal_of_comm addOrderOf_eq_pos_iff IsOfFinAddOrder.addOrderOf_pos
finite_setOf_addOrderOf_eq 📖	mathematical	—	Set.Finite AddCircle setOf addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddCommGroup.toAddGroup AddSubgroup.zmultiples AddSubgroup.normal_of_comm	—	Set.Finite.subset AddSubgroup.normal_of_comm finite_torsion addOrderOf_eq_iff
finite_torsion 📖	mathematical	—	Set.Finite AddCircle setOf AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddCommGroup.toAddGroup AddSubgroup.zmultiples AddSubgroup.normal_of_comm NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup	—	finite_torsion_of_isSMulRegular IsSMulRegular.of_right_eq_zero_of_smul instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add LT.lt.ne'
finite_torsion_of_isSMulRegular 📖	mathematical	IsSMulRegular AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	Set.Finite AddCircle setOf QuotientAddGroup.Quotient.addGroup AddSubgroup.zmultiples AddSubgroup.normal_of_comm NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim AddSubgroup.normal_of_comm Unique.instSubsingleton AddSubgroup.finite_quotient_of_finiteIndex AddSubgroup.finiteIndex_of_finite Finite.of_subsingleton eq_or_ne IsSMulRegular.not_zero ENat.card_lt_top LE.le.trans_lt card_torsion_le_of_isSMulRegular ENat.coe_lt_top
finite_torsion_of_isSMulRegular_int 📖	mathematical	IsSMulRegular SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	Set.Finite AddCircle setOf QuotientAddGroup.Quotient.addGroup AddSubgroup.zmultiples AddSubgroup.normal_of_comm NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim AddSubgroup.normal_of_comm Unique.instSubsingleton AddSubgroup.finite_quotient_of_finiteIndex AddSubgroup.finiteIndex_of_finite Finite.of_subsingleton eq_or_ne IsSMulRegular.not_zero ENat.card_lt_top LE.le.trans_lt card_torsion_le_of_isSMulRegular_int ENat.coe_lt_top
gcd_mul_addOrderOf_div_eq 📖	mathematical	—	addOrderOf HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing QuotientAddGroup.instHasQuotientAddSubgroup AddSubgroup.zmultiples SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	AddSubgroup.normal_of_comm natCast_div_mul_eq_nsmul IsOfFinAddOrder.addOrderOf_nsmul addOrderOf_pos_iff addOrderOf_period_div
homeomorphAddCircle_apply_mk 📖	mathematical	—	DFunLike.coe Homeomorph AddCircle Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples EquivLike.toFunLike Homeomorph.instEquivLike homeomorphAddCircle Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield	—	—
homeomorphAddCircle_symm_apply_mk 📖	mathematical	—	DFunLike.coe Homeomorph AddCircle Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm homeomorphAddCircle Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield	—	—
intCast_div_mul_eq_zsmul 📖	mathematical	—	AddCommGroup.toAddGroup Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing AddSubgroup.zmultiples Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddGroupWithOne.toIntCast Ring.toAddGroupWithOne HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup SubNegMonoid.toZSMul AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm	—	AddSubgroup.normal_of_comm mul_comm_div zsmul_eq_mul coe_zsmul
isOfFinAddOrder_iff_exists_rat_eq_div 📖	mathematical	—	IsOfFinAddOrder HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing QuotientAddGroup.instHasQuotientAddSubgroup AddSubgroup.zmultiples SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm DivisionRing.toRatCast DivInvMonoid.toDiv DivisionRing.toDivInvMonoid	—	AddSubgroup.normal_of_comm Iff.not_right not_isOfFinAddOrder_iff_forall_rat_ne_div
liftIco_coe_apply 📖	mathematical	Set Set.instMembership Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	liftIco AddCommGroup.toAddGroup AddSubgroup.zmultiples	—	equivIco_coe_eq
liftIco_comp_apply 📖	mathematical	—	liftIco	—	—
liftIco_continuous 📖	mathematical	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid ContinuousOn Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Continuous AddCircle QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples liftIco	—	liftIco_eq_lift_Icc Continuous.comp continuous_coinduced_dom continuousOn_iff_continuous_restrict Homeomorph.continuous_toFun
liftIco_eq_lift_Icc 📖	mathematical	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	liftIco AddCircle Set.Elem Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder EndpointIdent Set.restrict DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike equivIccQuot	—	—
liftIco_zero_coe_apply 📖	mathematical	Set Set.instMembership Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	liftIco AddCommGroup.toAddGroup AddSubgroup.zmultiples	—	liftIco_coe_apply zero_add
liftIco_zero_continuous 📖	mathematical	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContinuousOn Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Continuous AddCircle QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples liftIco	—	liftIco_continuous zero_add
liftIoc_coe_apply 📖	mathematical	Set Set.instMembership Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	liftIoc AddCommGroup.toAddGroup AddSubgroup.zmultiples	—	equivIoc_coe_eq
liftIoc_comp_apply 📖	mathematical	—	liftIoc	—	—
liftIoc_continuous 📖	mathematical	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid ContinuousOn Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Continuous AddCircle QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples liftIoc	—	liftIoc_eq_lift_Icc Continuous.comp continuous_coinduced_dom continuousOn_iff_continuous_restrict Homeomorph.continuous_toFun
liftIoc_eq_liftIco 📖	mathematical	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	liftIoc liftIco	—	Set.mem_univ coe_image_Ico_eq liftIco_coe_apply le_iff_eq_or_lt Set.mem_Ico coe_add_period liftIoc_coe_apply IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono contravariant_lt_of_covariant_le Fact.out LT.lt.le
liftIoc_eq_lift_Icc 📖	mathematical	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	liftIoc AddCircle Set.Elem Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder EndpointIdent Set.restrict DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike equivIccQuot	—	liftIco_eq_lift_Icc liftIoc_eq_liftIco
liftIoc_zero_coe_apply 📖	mathematical	Set Set.instMembership Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	liftIoc AddCommGroup.toAddGroup AddSubgroup.zmultiples	—	liftIoc_coe_apply zero_add
liftIoc_zero_continuous 📖	mathematical	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContinuousOn Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Continuous AddCircle QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples liftIoc	—	liftIoc_continuous zero_add
natCast_div_mul_eq_nsmul 📖	mathematical	—	AddCommGroup.toAddGroup Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing AddSubgroup.zmultiples Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm	—	AddSubgroup.normal_of_comm mul_comm_div nsmul_eq_mul coe_nsmul
not_isOfFinAddOrder_iff_forall_rat_ne_div 📖	mathematical	—	IsOfFinAddOrder HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing QuotientAddGroup.instHasQuotientAddSubgroup AddSubgroup.zmultiples SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm	—	AddSubgroup.normal_of_comm zsmul_eq_mul mul_comm eq_div_iff LT.lt.ne' Fact.out Rat.cast_div IsStrictOrderedRing.toCharZero Rat.cast_intCast div_mul_eq_mul_div
nsmul_eq_zero_iff 📖	mathematical	—	AddCircle Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddCommGroup.toAddGroup AddSubgroup.zmultiples AddSubgroup.normal_of_comm NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	AddSubgroup.normal_of_comm QuotientAddGroup.induction_on coe_eq_zero_iff coe_nsmul Int.natMod_lt LT.lt.ne' Nat.cast_ne_zero IsStrictOrderedRing.toCharZero mul_div_cancel_right₀ GroupWithZero.toMulDivCancelClass mul_comm mul_div mul_assoc Int.cast_natCast Int.cast_mul zsmul_eq_mul add_div add_smul div_eq_iff nsmul_eq_mul coe_add Int.natMod.eq_1 Nat.cast_zero Int.instCharZero mul_div_right_comm add_eq_right AddRightCancelSemigroup.toIsRightCancelAdd coe_zsmul coe_period smul_zero addOrderOf_dvd_iff_nsmul_eq_zero gcd_mul_addOrderOf_div_eq
openPartialHomeomorphCoe_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' AddCircle QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples openPartialHomeomorphCoe	—	—
openPartialHomeomorphCoe_source 📖	mathematical	—	PartialEquiv.source AddCircle OpenPartialHomeomorph.toPartialEquiv QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples openPartialHomeomorphCoe Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	—
openPartialHomeomorphCoe_symm_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' AddCircle QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples OpenPartialHomeomorph.symm openPartialHomeomorphCoe Set Set.instMembership Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid DFunLike.coe Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike equivIco	—	—
openPartialHomeomorphCoe_target 📖	mathematical	—	PartialEquiv.target AddCircle OpenPartialHomeomorph.toPartialEquiv QuotientAddGroup.instTopologicalSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples openPartialHomeomorphCoe Compl.compl Set Set.instCompl Set.instSingletonSet	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousAt_toIcoDiv 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddCommGroup.ModEq AddCommGroup.toAddCommMonoid	ContinuousAt instTopologicalSpaceInt toIcoDiv	—	tendsto_nhds_of_eventually_eq eventuallyEq_toIcoDiv_nhds
continuousAt_toIcoMod 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddCommGroup.ModEq AddCommGroup.toAddCommMonoid	ContinuousAt toIcoMod	—	ContinuousAt.sub IsTopologicalAddGroup.to_continuousSub LinearOrderedAddCommGroup.toIsTopologicalAddGroup continuousAt_id tendsto_nhds_of_eventually_eq Filter.EventuallyEq.fun_comp eventuallyEq_toIcoDiv_nhds
continuousAt_toIocDiv 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddCommGroup.ModEq AddCommGroup.toAddCommMonoid	ContinuousAt instTopologicalSpaceInt toIocDiv	—	tendsto_nhds_of_eventually_eq eventuallyEq_toIocDiv_nhds
continuousAt_toIocMod 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddCommGroup.ModEq AddCommGroup.toAddCommMonoid	ContinuousAt toIocMod	—	ContinuousAt.sub IsTopologicalAddGroup.to_continuousSub LinearOrderedAddCommGroup.toIsTopologicalAddGroup continuousAt_id tendsto_nhds_of_eventually_eq Filter.EventuallyEq.fun_comp eventuallyEq_toIocDiv_nhds
continuousOn_toIcoDiv 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	ContinuousOn instTopologicalSpaceInt toIcoDiv setOf AddCommGroup.ModEq AddCommGroup.toAddCommMonoid	—	ContinuousAt.continuousWithinAt continuousAt_toIcoDiv
continuousOn_toIocDiv 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	ContinuousOn instTopologicalSpaceInt toIocDiv setOf AddCommGroup.ModEq AddCommGroup.toAddCommMonoid	—	ContinuousAt.continuousWithinAt continuousAt_toIocDiv
continuousWithinAt_toIcoDiv_Ici 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	ContinuousWithinAt instTopologicalSpaceInt toIcoDiv Set.Ici	—	Filter.Tendsto.mono_right Filter.tendsto_pure eventuallyEq_toIcoDiv_nhdsGE pure_le_nhds
continuousWithinAt_toIcoMod_Ici 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	ContinuousWithinAt toIcoMod Set.Ici	—	ContinuousWithinAt.sub IsTopologicalAddGroup.to_continuousSub LinearOrderedAddCommGroup.toIsTopologicalAddGroup continuousWithinAt_id ContinuousWithinAt.smul AddGroup.continuousSMul_int continuousWithinAt_toIcoDiv_Ici continuousWithinAt_const
continuousWithinAt_toIocDiv_Iic 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	ContinuousWithinAt instTopologicalSpaceInt toIocDiv Set.Iic	—	Filter.Tendsto.mono_right Filter.tendsto_pure eventuallyEq_toIocDiv_nhdsLE pure_le_nhds
continuousWithinAt_toIocMod_Iic 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	ContinuousWithinAt toIocMod Set.Iic	—	ContinuousWithinAt.sub IsTopologicalAddGroup.to_continuousSub LinearOrderedAddCommGroup.toIsTopologicalAddGroup continuousWithinAt_id ContinuousWithinAt.smul AddGroup.continuousSMul_int continuousWithinAt_toIocDiv_Iic continuousWithinAt_const
continuous_left_toIocMod 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	ContinuousWithinAt toIocMod Set.Iic	—	continuousWithinAt_toIocMod_Iic
continuous_right_toIcoMod 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	ContinuousWithinAt toIcoMod Set.Ici	—	continuousWithinAt_toIcoMod_Ici
eventuallyEq_toIcoDiv_nhds 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddCommGroup.ModEq AddCommGroup.toAddCommMonoid	Filter.EventuallyEq nhds toIcoDiv	—	nhdsLT_sup_nhdsGE Filter.EventuallyEq.eq_1 Filter.eventually_sup AddCommGroup.not_modEq_iff_toIcoDiv_eq_toIocDiv AddCommGroup.modEq_comm Filter.EventuallyEq.eventually eventuallyEq_toIcoDiv_nhdsLT eventuallyEq_toIcoDiv_nhdsGE
eventuallyEq_toIcoDiv_nhdsGE 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Filter.EventuallyEq nhdsWithin Set.Ici toIcoDiv	—	Ico_mem_nhdsGE_of_mem instClosedIciTopology OrderTopology.to_orderClosedTopology Set.sub_mem_Ico_iff_left toIcoDiv_eq_iff
eventuallyEq_toIcoDiv_nhdsLT 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Filter.EventuallyEq nhdsWithin Set.Iio toIcoDiv toIocDiv	—	Ico_mem_nhdsLT_of_mem instClosedIicTopology OrderTopology.to_orderClosedTopology Set.sub_mem_Ioc_iff_left toIocDiv_eq_iff
eventuallyEq_toIocDiv_nhds 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddCommGroup.ModEq AddCommGroup.toAddCommMonoid	Filter.EventuallyEq nhds toIocDiv	—	nhdsLE_sup_nhdsGT Filter.EventuallyEq.eq_1 Filter.eventually_sup eventuallyEq_toIocDiv_nhdsLE AddCommGroup.not_modEq_iff_toIcoDiv_eq_toIocDiv AddCommGroup.modEq_comm Filter.EventuallyEq.eventually eventuallyEq_toIocDiv_nhdsGT
eventuallyEq_toIocDiv_nhdsGT 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Filter.EventuallyEq nhdsWithin Set.Ioi toIocDiv toIcoDiv	—	Ioc_mem_nhdsGT_of_mem instClosedIciTopology OrderTopology.to_orderClosedTopology Set.sub_mem_Ico_iff_left toIcoDiv_eq_iff
eventuallyEq_toIocDiv_nhdsLE 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Filter.EventuallyEq nhdsWithin Set.Iic toIocDiv	—	Ioc_mem_nhdsLE_of_mem instClosedIicTopology OrderTopology.to_orderClosedTopology Set.sub_mem_Ioc_iff_left toIocDiv_eq_iff
toIcoMod_eventuallyEq_toIocMod 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddCommGroup.ModEq AddCommGroup.toAddCommMonoid	Filter.EventuallyEq nhds toIcoMod toIocMod	—	IsOpen.mem_nhds Ico_eq_locus_Ioc_eq_iUnion_Ioo isOpen_iUnion isOpen_Ioo OrderTopology.to_orderClosedTopology Set.mem_setOf_eq AddCommGroup.not_modEq_iff_toIcoMod_eq_toIocMod AddCommGroup.modEq_comm

---

← Back to Index