ToIntervalMod

📁 Source: Mathlib/Algebra/Order/ToIntervalMod.lean

Statistics

Metric	Count
Definitions `circularOrder`, `circularPreorder`, `equivIcoMod`, `equivIocMod`, `instBtwQuotientAddSubgroupZmultiples`, `toIcoDiv`, `toIcoMod`, `toIocDiv`, `toIocMod`	9
Theorems `toIcoMod_eq_left`, `toIcoMod_eq_right`, `toIcoMod_eq_toIcoMod`, `modEq_iff_forall_notMem_Ioo_mod`, `modEq_iff_toIcoDiv_eq_toIocDiv_add_one`, `modEq_iff_toIcoMod_add_period_eq_toIocMod`, `modEq_iff_toIcoMod_eq_left`, `modEq_iff_toIcoMod_ne_toIocMod`, `modEq_iff_toIocMod_eq_right`, `not_modEq_iff_toIcoDiv_eq_toIocDiv`, `not_modEq_iff_toIcoMod_eq_toIocMod`, `tfae_modEq`, `Ico_eq_locus_Ioc_eq_iUnion_Ioo`, `btw_coe_iff`, `btw_coe_iff'`, `equivIcoMod_coe`, `equivIcoMod_symm_apply`, `equivIcoMod_zero`, `equivIocMod_coe`, `equivIocMod_symm_apply`, `equivIocMod_zero`, `iUnion_Icc_add_intCast`, `iUnion_Icc_add_zsmul`, `iUnion_Icc_intCast`, `iUnion_Icc_zsmul`, `iUnion_Ico_add_intCast`, `iUnion_Ico_add_zsmul`, `iUnion_Ico_intCast`, `iUnion_Ico_zsmul`, `iUnion_Ioc_add_intCast`, `iUnion_Ioc_add_zsmul`, `iUnion_Ioc_intCast`, `iUnion_Ioc_zsmul`, `left_le_toIcoMod`, `left_lt_toIocMod`, `self_sub_toIcoDiv_mul`, `self_sub_toIcoDiv_zsmul`, `self_sub_toIcoMod`, `self_sub_toIcoMod_eq_mul`, `self_sub_toIocDiv_mul`, `self_sub_toIocDiv_zsmul`, `self_sub_toIocMod`, `self_sub_toIocMod_eq_mul`, `sub_toIcoDiv_zsmul_mem_Ico`, `sub_toIocDiv_zsmul_mem_Ioc`, `toIcoDiv_add_intCast_mul`, `toIcoDiv_add_intCast_mul'`, `toIcoDiv_add_left`, `toIcoDiv_add_left'`, `toIcoDiv_add_natCast_mul`, `toIcoDiv_add_natCast_mul'`, `toIcoDiv_add_nsmul`, `toIcoDiv_add_nsmul'`, `toIcoDiv_add_ofNat_mul`, `toIcoDiv_add_ofNat_mul'`, `toIcoDiv_add_right`, `toIcoDiv_add_right'`, `toIcoDiv_add_zsmul`, `toIcoDiv_add_zsmul'`, `toIcoDiv_apply_left`, `toIcoDiv_apply_right`, `toIcoDiv_eq_floor`, `toIcoDiv_eq_iff`, `toIcoDiv_eq_of_sub_zsmul_mem_Ico`, `toIcoDiv_eq_sub`, `toIcoDiv_intCast_mul_add`, `toIcoDiv_mul_sub_self`, `toIcoDiv_mul_sub_toIcoMod`, `toIcoDiv_natCast_mul_add`, `toIcoDiv_neg`, `toIcoDiv_neg'`, `toIcoDiv_nsmul_add`, `toIcoDiv_ofNat_mul_add`, `toIcoDiv_sub`, `toIcoDiv_sub'`, `toIcoDiv_sub_eq_toIcoDiv_add`, `toIcoDiv_sub_eq_toIcoDiv_add'`, `toIcoDiv_sub_intCast_mul`, `toIcoDiv_sub_intCast_mul'`, `toIcoDiv_sub_natCast_mul`, `toIcoDiv_sub_natCast_mul'`, `toIcoDiv_sub_nsmul`, `toIcoDiv_sub_nsmul'`, `toIcoDiv_sub_ofNat_mul`, `toIcoDiv_sub_ofNat_mul'`, `toIcoDiv_sub_zsmul`, `toIcoDiv_sub_zsmul'`, `toIcoDiv_zero_one`, `toIcoDiv_zsmul_add`, `toIcoDiv_zsmul_sub_self`, `toIcoDiv_zsmul_sub_toIcoMod`, `toIcoMod_add_intCast_mul`, `toIcoMod_add_intCast_mul'`, `toIcoMod_add_left`, `toIcoMod_add_left'`, `toIcoMod_add_natCast_mul`, `toIcoMod_add_natCast_mul'`, `toIcoMod_add_nsmul`, `toIcoMod_add_nsmul'`, `toIcoMod_add_ofNat_mul`, `toIcoMod_add_ofNat_mul'`, `toIcoMod_add_right`, `toIcoMod_add_right'`, `toIcoMod_add_right_eq_add`, `toIcoMod_add_toIcoDiv_mul`, `toIcoMod_add_toIcoDiv_zsmul`, `toIcoMod_add_toIocMod_zero`, `toIcoMod_add_zsmul`, `toIcoMod_add_zsmul'`, `toIcoMod_apply_left`, `toIcoMod_apply_right`, `toIcoMod_eq_add_fract_mul`, `toIcoMod_eq_fract_mul`, `toIcoMod_eq_iff`, `toIcoMod_eq_self`, `toIcoMod_eq_sub`, `toIcoMod_eq_toIcoMod`, `toIcoMod_inj`, `toIcoMod_intCast_mul_add`, `toIcoMod_intCast_mul_add'`, `toIcoMod_le_toIocMod`, `toIcoMod_lt_right`, `toIcoMod_mem_Ico`, `toIcoMod_mem_Ico'`, `toIcoMod_natCast_mul_add`, `toIcoMod_natCast_mul_add'`, `toIcoMod_neg`, `toIcoMod_neg'`, `toIcoMod_nsmul_add`, `toIcoMod_nsmul_add'`, `toIcoMod_ofNat_mul_add`, `toIcoMod_ofNat_mul_add'`, `toIcoMod_periodic`, `toIcoMod_sub`, `toIcoMod_sub'`, `toIcoMod_sub_eq_sub`, `toIcoMod_sub_intCast_mul`, `toIcoMod_sub_intCast_mul'`, `toIcoMod_sub_natCast_mul`, `toIcoMod_sub_natCast_mul'`, `toIcoMod_sub_nsmul`, `toIcoMod_sub_nsmul'`, `toIcoMod_sub_ofNat_mul`, `toIcoMod_sub_ofNat_mul'`, `toIcoMod_sub_self`, `toIcoMod_sub_self_eq_mul`, `toIcoMod_sub_zsmul`, `toIcoMod_sub_zsmul'`, `toIcoMod_toIcoMod`, `toIcoMod_toIocMod`, `toIcoMod_zero_one`, `toIcoMod_zero_sub_comm`, `toIcoMod_zsmul_add`, `toIcoMod_zsmul_add'`, `toIocDiv_add_intCast_mul`, `toIocDiv_add_intCast_mul'`, `toIocDiv_add_left`, `toIocDiv_add_left'`, `toIocDiv_add_natCast_mul`, `toIocDiv_add_natCast_mul'`, `toIocDiv_add_nsmul`, `toIocDiv_add_nsmul'`, `toIocDiv_add_ofNat_mul`, `toIocDiv_add_ofNat_mul'`, `toIocDiv_add_right`, `toIocDiv_add_right'`, `toIocDiv_add_zsmul`, `toIocDiv_add_zsmul'`, `toIocDiv_apply_left`, `toIocDiv_apply_right`, `toIocDiv_eq_iff`, `toIocDiv_eq_neg_floor`, `toIocDiv_eq_of_sub_zsmul_mem_Ioc`, `toIocDiv_eq_sub`, `toIocDiv_intCast_mul_add`, `toIocDiv_mul_sub_self`, `toIocDiv_mul_sub_toIocMod`, `toIocDiv_natCast_mul_add`, `toIocDiv_neg`, `toIocDiv_neg'`, `toIocDiv_nsmul_add`, `toIocDiv_ofNat_mul_add`, `toIocDiv_sub`, `toIocDiv_sub'`, `toIocDiv_sub_eq_toIocDiv_add`, `toIocDiv_sub_eq_toIocDiv_add'`, `toIocDiv_sub_intCast_mul`, `toIocDiv_sub_intCast_mul'`, `toIocDiv_sub_natCast_mul`, `toIocDiv_sub_natCast_mul'`, `toIocDiv_sub_nsmul`, `toIocDiv_sub_nsmul'`, `toIocDiv_sub_ofNat_mul`, `toIocDiv_sub_ofNat_mul'`, `toIocDiv_sub_zsmul`, `toIocDiv_sub_zsmul'`, `toIocDiv_wcovBy_toIcoDiv`, `toIocDiv_zsmul_add`, `toIocDiv_zsmul_sub_self`, `toIocDiv_zsmul_sub_toIocMod`, `toIocMod_add_intCast_mul`, `toIocMod_add_intCast_mul'`, `toIocMod_add_left`, `toIocMod_add_left'`, `toIocMod_add_natCast_mul`, `toIocMod_add_natCast_mul'`, `toIocMod_add_nsmul`, `toIocMod_add_nsmul'`, `toIocMod_add_ofNat_mul`, `toIocMod_add_ofNat_mul'`, `toIocMod_add_right`, `toIocMod_add_right'`, `toIocMod_add_right_eq_add`, `toIocMod_add_toIcoMod_zero`, `toIocMod_add_toIocDiv_mul`, `toIocMod_add_toIocDiv_zsmul`, `toIocMod_add_zsmul`, `toIocMod_add_zsmul'`, `toIocMod_apply_left`, `toIocMod_apply_right`, `toIocMod_eq_iff`, `toIocMod_eq_self`, `toIocMod_eq_sub`, `toIocMod_eq_sub_fract_mul`, `toIocMod_eq_toIocMod`, `toIocMod_intCast_mul_add`, `toIocMod_intCast_mul_add'`, `toIocMod_le_right`, `toIocMod_le_toIcoMod_add`, `toIocMod_mem_Ioc`, `toIocMod_natCast_mul_add`, `toIocMod_natCast_mul_add'`, `toIocMod_neg`, `toIocMod_neg'`, `toIocMod_nsmul_add`, `toIocMod_nsmul_add'`, `toIocMod_ofNat_mul_add`, `toIocMod_ofNat_mul_add'`, `toIocMod_periodic`, `toIocMod_sub`, `toIocMod_sub'`, `toIocMod_sub_eq_sub`, `toIocMod_sub_intCast_mul`, `toIocMod_sub_intCast_mul'`, `toIocMod_sub_natCast_mul`, `toIocMod_sub_natCast_mul'`, `toIocMod_sub_nsmul`, `toIocMod_sub_nsmul'`, `toIocMod_sub_ofNat_mul`, `toIocMod_sub_ofNat_mul'`, `toIocMod_sub_self`, `toIocMod_sub_self_eq_mul`, `toIocMod_sub_zsmul`, `toIocMod_sub_zsmul'`, `toIocMod_toIcoMod`, `toIocMod_toIocMod`, `toIocMod_zero_sub_comm`, `toIocMod_zsmul_add`, `toIocMod_zsmul_add'`	259
Total	268

AddCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`modEq_iff_forall_notMem_Ioo_mod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `toDivisionAddCommMonoid`	`ModEq` `toAddCommMonoid` `Set` `Set.instMembership` `Set.Ioo` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `toAddGroup` `SubNegMonoid.toZSMul`	—	`List.TFAE.out` `tfae_modEq`
`modEq_iff_toIcoDiv_eq_toIocDiv_add_one` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `toDivisionAddCommMonoid`	`ModEq` `toAddCommMonoid` `toIcoDiv` `toIocDiv`	—	`modEq_iff_toIcoMod_add_period_eq_toIocMod` `toIcoMod.eq_1` `toIocMod.eq_1` `eq_sub_iff_add_eq` `sub_sub` `add_one_zsmul`
`modEq_iff_toIcoMod_add_period_eq_toIocMod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `toDivisionAddCommMonoid`	`ModEq` `toAddCommMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `toIcoMod` `toIocMod`	—	`List.TFAE.out` `tfae_modEq`
`modEq_iff_toIcoMod_eq_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `toDivisionAddCommMonoid`	`ModEq` `toAddCommMonoid` `toIcoMod`	—	`modEq_iff_eq_add_zsmul` `toIcoMod_add_zsmul` `toIcoMod_apply_left` `eq_add_of_sub_eq`
`modEq_iff_toIcoMod_ne_toIocMod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `toDivisionAddCommMonoid`	`ModEq` `toAddCommMonoid`	—	`List.TFAE.out` `tfae_modEq`
`modEq_iff_toIocMod_eq_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `toDivisionAddCommMonoid`	`ModEq` `toAddCommMonoid` `toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`modEq_iff_eq_add_zsmul` `toIocMod_add_zsmul` `toIocMod_apply_left` `add_one_zsmul` `add_left_comm` `sub_eq_iff_eq_add'`
`not_modEq_iff_toIcoDiv_eq_toIocDiv` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `toDivisionAddCommMonoid`	`ModEq` `toAddCommMonoid` `toIcoDiv` `toIocDiv`	—	`not_modEq_iff_toIcoMod_eq_toIocMod` `toIcoMod.eq_1` `toIocMod.eq_1`
`not_modEq_iff_toIcoMod_eq_toIocMod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `toDivisionAddCommMonoid`	`ModEq` `toAddCommMonoid` `toIcoMod` `toIocMod`	—	`Iff.not_left` `modEq_iff_toIcoMod_ne_toIocMod`
`tfae_modEq` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `toDivisionAddCommMonoid`	`List.TFAE` `ModEq` `toAddCommMonoid` `toIcoMod` `toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`modEq_iff_toIcoMod_eq_left` `not_imp_not` `toIcoMod_eq_iff` `Set.Ioo_subset_Ico_self` `sub_add_cancel` `toIocMod_eq_iff` `Set.Ioo_subset_Ioc_self` `add_eq_left` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `LT.lt.ne'` `Set.right_mem_Ioc` `lt_add_of_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `sub_one_zsmul` `add_add_add_comm` `add_neg_cancel` `add_zero` `toIcoMod_add_toIcoDiv_zsmul` `not_imp_comm` `toIcoMod_mem_Ico` `LE.le.lt_of_ne'` `List.tfae_of_cycle`

AddCommGroup.ModEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toIcoMod_eq_left` 📖	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`	`toIcoMod`	—	`AddCommGroup.modEq_iff_toIcoMod_eq_left`
`toIcoMod_eq_right` 📖	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`	`toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`AddCommGroup.modEq_iff_toIocMod_eq_right`
`toIcoMod_eq_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`	`toIcoMod`	—	—

QuotientAddGroup

Definitions

Name	Category	Theorems
`circularOrder` 📖	CompOp	—
`circularPreorder` 📖	CompOp	—
`equivIcoMod` 📖	CompOp	3 math math: `equivIcoMod_symm_apply`, `equivIcoMod_zero`, `equivIcoMod_coe`
`equivIocMod` 📖	CompOp	3 math math: `equivIocMod_zero`, `equivIocMod_symm_apply`, `equivIocMod_coe`
`instBtwQuotientAddSubgroupZmultiples` 📖	CompOp	2 math math: `btw_coe_iff`, `btw_coe_iff'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`btw_coe_iff` 📖	mathematical	—	`Btw.btw` `HasQuotient.Quotient` `AddSubgroup` `AddCommGroup.toAddGroup` `instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `instBtwQuotientAddSubgroupZmultiples` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `toIcoMod` `Fact.out` `Preorder.toLT` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `toIocMod`	—	`Fact.out` `btw_coe_iff'` `toIocMod_sub_eq_sub` `toIcoMod_sub_eq_sub` `zero_add` `sub_le_sub_iff_right` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono`
`btw_coe_iff'` 📖	mathematical	—	`Btw.btw` `HasQuotient.Quotient` `AddSubgroup` `AddCommGroup.toAddGroup` `instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `instBtwQuotientAddSubgroupZmultiples` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `toIcoMod` `Fact.out` `Preorder.toLT` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `toIocMod`	—	—
`equivIcoMod_coe` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`DFunLike.coe` `Equiv` `HasQuotient.Quotient` `AddSubgroup` `AddCommGroup.toAddGroup` `instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `Set.Elem` `Set.Ico` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivIcoMod` `Set` `Set.instMembership` `toIcoMod` `toIcoMod_mem_Ico`	—	—
`equivIcoMod_symm_apply` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`DFunLike.coe` `Equiv` `Set.Elem` `Set.Ico` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `HasQuotient.Quotient` `AddSubgroup` `AddCommGroup.toAddGroup` `instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivIcoMod` `Set` `Set.instMembership`	—	—
`equivIcoMod_zero` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`DFunLike.coe` `Equiv` `HasQuotient.Quotient` `AddSubgroup` `AddCommGroup.toAddGroup` `instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `Set.Elem` `Set.Ico` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivIcoMod` `Quotient.addCommGroup` `Set` `Set.instMembership` `toIcoMod` `toIcoMod_mem_Ico`	—	—
`equivIocMod_coe` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`DFunLike.coe` `Equiv` `HasQuotient.Quotient` `AddSubgroup` `AddCommGroup.toAddGroup` `instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `Set.Elem` `Set.Ioc` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivIocMod` `Set` `Set.instMembership` `toIocMod` `toIocMod_mem_Ioc`	—	—
`equivIocMod_symm_apply` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`DFunLike.coe` `Equiv` `Set.Elem` `Set.Ioc` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `HasQuotient.Quotient` `AddSubgroup` `AddCommGroup.toAddGroup` `instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivIocMod` `Set` `Set.instMembership`	—	—
`equivIocMod_zero` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`DFunLike.coe` `Equiv` `HasQuotient.Quotient` `AddSubgroup` `AddCommGroup.toAddGroup` `instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `Set.Elem` `Set.Ioc` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivIocMod` `Quotient.addCommGroup` `Set` `Set.instMembership` `toIocMod` `toIocMod_mem_Ioc`	—	—

(root)

Definitions

Name	Category	Theorems
`toIcoDiv` 📖	CompOp	67 math math: `toIcoDiv_mul_sub_self`, `toIcoDiv_sub_natCast_mul'`, `toIcoDiv_add_intCast_mul'`, `toIcoDiv_sub_intCast_mul'`, `toIcoDiv_zsmul_sub_toIcoMod`, `toIcoDiv_mul_sub_toIcoMod`, `toIcoDiv_intCast_mul_add`, `toIcoDiv_eq_of_sub_zsmul_mem_Ico`, `toIcoDiv_sub'`, `toIcoMod_sub_self_eq_mul`, `toIocDiv_wcovBy_toIcoDiv`, `toIcoDiv_add_left'`, `self_sub_toIcoDiv_zsmul`, `eventuallyEq_toIcoDiv_nhds`, `self_sub_toIcoMod_eq_mul`, `toIcoDiv_add_nsmul`, `toIcoDiv_sub_eq_toIcoDiv_add`, `eventuallyEq_toIocDiv_nhdsGT`, `toIocDiv_neg'`, `toIcoDiv_sub`, `AddCommGroup.not_modEq_iff_toIcoDiv_eq_toIocDiv`, `toIcoDiv_zsmul_add`, `toIcoDiv_zero_one`, `toIcoDiv_apply_right`, `toIcoDiv_add_zsmul`, `toIcoDiv_add_ofNat_mul`, `toIcoMod_sub_self`, `toIcoDiv_add_natCast_mul`, `eventuallyEq_toIcoDiv_nhdsLT`, `self_sub_toIcoDiv_mul`, `toIcoDiv_zsmul_sub_self`, `toIcoDiv_add_right`, `AddCommGroup.modEq_iff_toIcoDiv_eq_toIocDiv_add_one`, `sub_toIcoDiv_zsmul_mem_Ico`, `toIcoDiv_add_right'`, `self_sub_toIcoMod`, `eventuallyEq_toIcoDiv_nhdsGE`, `toIcoMod_add_toIcoDiv_mul`, `toIcoDiv_sub_eq_toIcoDiv_add'`, `continuousAt_toIcoDiv`, `toIcoDiv_add_intCast_mul`, `toIcoDiv_add_zsmul'`, `toIcoDiv_sub_ofNat_mul`, `toIcoDiv_eq_iff`, `toIocDiv_neg`, `toIcoDiv_neg`, `toIcoDiv_sub_zsmul`, `toIcoDiv_eq_floor`, `toIcoDiv_neg'`, `toIcoDiv_sub_natCast_mul`, `toIcoDiv_add_nsmul'`, `continuousOn_toIcoDiv`, `toIcoDiv_eq_sub`, `toIcoDiv_apply_left`, `toIcoDiv_sub_intCast_mul`, `toIcoMod_add_toIcoDiv_zsmul`, `toIcoDiv_add_natCast_mul'`, `toIcoDiv_natCast_mul_add`, `continuousWithinAt_toIcoDiv_Ici`, `toIcoDiv_sub_nsmul`, `toIcoDiv_add_ofNat_mul'`, `toIcoDiv_sub_nsmul'`, `toIcoDiv_sub_ofNat_mul'`, `toIcoDiv_sub_zsmul'`, `toIcoDiv_add_left`, `toIcoDiv_nsmul_add`, `toIcoDiv_ofNat_mul_add`
`toIcoMod` 📖	CompOp	95 math math: `toIcoMod_nsmul_add'`, `toIcoMod_ofNat_mul_add'`, `toIcoMod_eventuallyEq_toIocMod`, `toIcoDiv_mul_sub_self`, `toIcoMod_eq_fract_mul`, `AddCommGroup.modEq_iff_toIcoMod_eq_left`, `AddCircle.equivIccQuot_comp_mk_eq_toIcoMod`, `toIcoMod_inj`, `toIcoMod_sub`, `toIcoDiv_zsmul_sub_toIcoMod`, `toIcoMod_add_toIocMod_zero`, `AddCommGroup.not_modEq_iff_toIcoMod_eq_toIocMod`, `toIcoDiv_mul_sub_toIcoMod`, `toIcoMod_sub_zsmul`, `toIcoMod_eq_self`, `toIcoMod_add_natCast_mul`, `continuous_right_toIcoMod`, `toIcoMod_eq_toIcoMod`, `toIcoMod_sub'`, `continuousWithinAt_toIcoMod_Ici`, `toIcoMod_sub_self_eq_mul`, `AddCommGroup.modEq_iff_toIcoMod_add_period_eq_toIocMod`, `self_sub_toIcoDiv_zsmul`, `toIcoMod_sub_eq_sub`, `toIcoMod_apply_right`, `toIcoMod_add_intCast_mul`, `self_sub_toIcoMod_eq_mul`, `toIcoMod_neg`, `toIocMod_neg`, `AddCommGroup.ModEq.toIcoMod_eq_left`, `AddCommGroup.ModEq.toIcoMod_eq_toIcoMod`, `toIcoMod_add_zsmul`, `toIcoMod_add_intCast_mul'`, `toIcoMod_add_right`, `toIcoMod_eq_iff`, `toIcoMod_lt_right`, `toIcoMod_eq_add_fract_mul`, `Ico_eq_locus_Ioc_eq_iUnion_Ioo`, `toIcoMod_sub_natCast_mul'`, `continuousAt_toIcoMod`, `toIcoMod_sub_intCast_mul`, `toIcoMod_add_left`, `toIcoMod_sub_nsmul`, `toIcoMod_zero_sub_comm`, `toIcoMod_sub_self`, `toIcoMod_sub_ofNat_mul'`, `toIcoMod_eq_sub`, `toIcoMod_add_nsmul'`, `toIcoMod_sub_nsmul'`, `self_sub_toIcoDiv_mul`, `toIcoDiv_zsmul_sub_self`, `toIcoMod_add_right'`, `toIcoMod_sub_intCast_mul'`, `toIcoMod_add_natCast_mul'`, `QuotientAddGroup.btw_coe_iff`, `toIcoMod_zsmul_add'`, `toIcoMod_sub_natCast_mul`, `toIcoMod_add_nsmul`, `self_sub_toIcoMod`, `toIcoMod_mem_Ico`, `toIcoMod_add_right_eq_add`, `toIcoMod_add_toIcoDiv_mul`, `QuotientAddGroup.btw_coe_iff'`, `toIcoMod_natCast_mul_add`, `toIocMod_le_toIcoMod_add`, `toIcoMod_apply_left`, `toIcoMod_neg'`, `toIcoMod_sub_zsmul'`, `toIcoMod_toIcoMod`, `Real.Angle.coe_toIcoMod`, `toIcoMod_intCast_mul_add`, `toIcoMod_add_left'`, `toIocMod_toIcoMod`, `toIcoMod_periodic`, `toIcoMod_add_ofNat_mul`, `toIcoMod_zero_one`, `AddCommGroup.tfae_modEq`, `toIcoMod_zsmul_add`, `QuotientAddGroup.equivIcoMod_zero`, `QuotientAddGroup.equivIcoMod_coe`, `toIcoMod_nsmul_add`, `toIcoMod_le_toIocMod`, `toIcoMod_add_toIcoDiv_zsmul`, `toIcoMod_add_zsmul'`, `toIocMod_neg'`, `toIcoMod_ofNat_mul_add`, `toIcoMod_add_ofNat_mul'`, `toIcoMod_mem_Ico'`, `left_le_toIcoMod`, `toIcoMod_toIocMod`, `toIocMod_zero_sub_comm`, `toIcoMod_natCast_mul_add'`, `toIcoMod_intCast_mul_add'`, `toIocMod_add_toIcoMod_zero`, `toIcoMod_sub_ofNat_mul`
`toIocDiv` 📖	CompOp	67 math math: `toIocDiv_sub_nsmul'`, `toIocMod_sub_self_eq_mul`, `toIocDiv_add_intCast_mul'`, `self_sub_toIocMod_eq_mul`, `toIocDiv_add_right'`, `toIocDiv_eq_of_sub_zsmul_mem_Ioc`, `toIocDiv_add_nsmul'`, `toIocDiv_sub_eq_toIocDiv_add`, `toIocDiv_wcovBy_toIcoDiv`, `toIocDiv_zsmul_sub_self`, `toIocDiv_natCast_mul_add`, `toIocMod_add_toIocDiv_zsmul`, `continuousAt_toIocDiv`, `self_sub_toIocMod`, `self_sub_toIocDiv_mul`, `eventuallyEq_toIocDiv_nhdsGT`, `toIocDiv_neg'`, `toIocDiv_apply_right`, `toIocDiv_add_ofNat_mul'`, `Complex.log_exp_eq_sub_toIocDiv`, `AddCommGroup.not_modEq_iff_toIcoDiv_eq_toIocDiv`, `toIocDiv_add_ofNat_mul`, `toIocDiv_sub_natCast_mul`, `toIocDiv_sub_nsmul`, `toIocDiv_mul_sub_toIocMod`, `toIocMod_sub_self`, `toIocDiv_sub_ofNat_mul`, `toIocDiv_sub`, `toIocDiv_add_left'`, `eventuallyEq_toIcoDiv_nhdsLT`, `toIocDiv_zsmul_add`, `AddCommGroup.modEq_iff_toIcoDiv_eq_toIocDiv_add_one`, `toIocDiv_sub_zsmul`, `toIocDiv_eq_neg_floor`, `self_sub_toIocDiv_zsmul`, `toIocDiv_sub_zsmul'`, `toIocDiv_zsmul_sub_toIocMod`, `continuousWithinAt_toIocDiv_Iic`, `toIocDiv_apply_left`, `toIocDiv_add_intCast_mul`, `toIocDiv_sub'`, `sub_toIocDiv_zsmul_mem_Ioc`, `toIocDiv_ofNat_mul_add`, `toIocDiv_sub_natCast_mul'`, `toIocDiv_add_nsmul`, `toIocDiv_intCast_mul_add`, `toIocDiv_add_natCast_mul'`, `toIocDiv_neg`, `toIocDiv_add_zsmul'`, `toIocDiv_sub_intCast_mul'`, `toIcoDiv_neg`, `eventuallyEq_toIocDiv_nhds`, `continuousOn_toIocDiv`, `toIcoDiv_neg'`, `eventuallyEq_toIocDiv_nhdsLE`, `toIocDiv_add_left`, `toIocDiv_sub_intCast_mul`, `toIocDiv_nsmul_add`, `toIocMod_add_toIocDiv_mul`, `toIocDiv_add_zsmul`, `toIocDiv_sub_ofNat_mul'`, `toIocDiv_eq_sub`, `toIocDiv_add_natCast_mul`, `toIocDiv_eq_iff`, `toIocDiv_sub_eq_toIocDiv_add'`, `toIocDiv_mul_sub_self`, `toIocDiv_add_right`
`toIocMod` 📖	CompOp	100 math math: `toIocMod_intCast_mul_add`, `toIcoMod_eventuallyEq_toIocMod`, `toIocMod_periodic`, `toIocMod_eq_self`, `continuousAt_toIocMod`, `toIocMod_sub_nsmul`, `toIocMod_sub_self_eq_mul`, `Complex.angle_exp_one`, `toIcoMod_add_toIocMod_zero`, `self_sub_toIocMod_eq_mul`, `AddCommGroup.not_modEq_iff_toIcoMod_eq_toIocMod`, `toIocMod_sub_natCast_mul'`, `QuotientAddGroup.equivIocMod_zero`, `Real.Angle.toReal_coe`, `toIocMod_sub'`, `toIocMod_add_intCast_mul'`, `Complex.log_exp_eq_re_add_toIocMod`, `toIocMod_sub_natCast_mul`, `toIocDiv_zsmul_sub_self`, `AddCommGroup.modEq_iff_toIcoMod_add_period_eq_toIocMod`, `toIocMod_zsmul_add'`, `toIocMod_add_toIocDiv_zsmul`, `toIocMod_natCast_mul_add`, `self_sub_toIocMod`, `continuous_left_toIocMod`, `self_sub_toIocDiv_mul`, `toIocMod_ofNat_mul_add'`, `toIocMod_sub_intCast_mul'`, `Complex.arg_mul_cos_add_sin_mul_I_eq_toIocMod`, `toIcoMod_neg`, `toIocMod_neg`, `toIocMod_ofNat_mul_add`, `left_lt_toIocMod`, `toIocMod_add_intCast_mul`, `toIocMod_add_natCast_mul'`, `toIocMod_sub_nsmul'`, `toIocMod_sub_eq_sub`, `AddCircle.equivIccQuot_comp_mk_eq_toIocMod`, `toIocMod_toIocMod`, `Complex.arg_exp_mul_I`, `toIocMod_eq_sub_fract_mul`, `Ico_eq_locus_Ioc_eq_iUnion_Ioo`, `toIocMod_apply_left`, `toIocMod_add_zsmul'`, `toIocMod_apply_right`, `toIocMod_sub`, `toIcoMod_zero_sub_comm`, `toIocDiv_mul_sub_toIocMod`, `AddCommGroup.ModEq.toIcoMod_eq_right`, `toIocMod_sub_self`, `toIocMod_add_ofNat_mul'`, `toIocMod_sub_ofNat_mul`, `toIocMod_nsmul_add'`, `QuotientAddGroup.btw_coe_iff`, `toIocMod_add_right`, `toIocMod_natCast_mul_add'`, `toIocMod_eq_sub`, `toIocMod_add_left`, `self_sub_toIocDiv_zsmul`, `toIocDiv_zsmul_sub_toIocMod`, `Complex.toIocMod_arg`, `Real.Angle.coe_toIocMod`, `toIocMod_eq_iff`, `QuotientAddGroup.btw_coe_iff'`, `toIocMod_add_nsmul'`, `toIocMod_le_right`, `toIocMod_eq_toIocMod`, `Real.Angle.toIocMod_toReal`, `toIocMod_add_left'`, `toIocMod_le_toIcoMod_add`, `toIcoMod_neg'`, `AddCommGroup.modEq_iff_toIocMod_eq_right`, `toIocMod_add_right_eq_add`, `toIocMod_nsmul_add`, `toIocMod_add_right'`, `toIocMod_toIcoMod`, `toIocMod_mem_Ioc`, `AddCommGroup.tfae_modEq`, `toIocMod_zsmul_add`, `toIocMod_sub_zsmul`, `toIocMod_intCast_mul_add'`, `toIocMod_add_nsmul`, `toIocMod_add_natCast_mul`, `toIocMod_sub_ofNat_mul'`, `toIocMod_add_toIocDiv_mul`, `toIcoMod_le_toIocMod`, `Complex.arg_exp`, `continuousWithinAt_toIocMod_Iic`, `toIocMod_neg'`, `toIocMod_add_zsmul`, `toIocMod_sub_zsmul'`, `toIocMod_add_ofNat_mul`, `toIcoMod_toIocMod`, `toIocMod_zero_sub_comm`, `Complex.arg_cos_add_sin_mul_I_eq_toIocMod`, `toIocMod_add_toIcoMod_zero`, `toIocDiv_mul_sub_self`, `QuotientAddGroup.equivIocMod_coe`, `Complex.angle_exp_exp`, `toIocMod_sub_intCast_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Ico_eq_locus_Ioc_eq_iUnion_Ioo` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`setOf` `toIcoMod` `toIocMod` `Set.iUnion` `Set.Ioo` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`Set.ext` `AddCommGroup.modEq_iff_forall_notMem_Ioo_mod`
`iUnion_Icc_add_intCast` 📖	mathematical	—	`Set.iUnion` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Set.univ`	—	`zsmul_one` `Int.cast_add` `Int.cast_one` `iUnion_Icc_add_zsmul` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`iUnion_Icc_add_zsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Set.iUnion` `Set.Icc` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Set.univ`	—	`iUnion_Ioc_add_zsmul` `Set.iUnion_mono` `Set.Ioc_subset_Icc_self`
`iUnion_Icc_intCast` 📖	mathematical	—	`Set.iUnion` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Set.univ`	—	`zero_add` `iUnion_Icc_add_intCast`
`iUnion_Icc_zsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Set.iUnion` `Set.Icc` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Set.univ`	—	`zero_add` `iUnion_Icc_add_zsmul`
`iUnion_Ico_add_intCast` 📖	mathematical	—	`Set.iUnion` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Set.univ`	—	`zsmul_one` `Int.cast_add` `Int.cast_one` `iUnion_Ico_add_zsmul` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`iUnion_Ico_add_zsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Set.iUnion` `Set.Ico` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Set.univ`	—	`Set.eq_univ_iff_forall` `Set.mem_iUnion` `sub_toIcoDiv_zsmul_mem_Ico` `le_sub_iff_add_le` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `add_smul` `one_smul` `add_assoc` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `sub_lt_iff_lt_add` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd`
`iUnion_Ico_intCast` 📖	mathematical	—	`Set.iUnion` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Set.univ`	—	`zero_add` `iUnion_Ico_add_intCast`
`iUnion_Ico_zsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Set.iUnion` `Set.Ico` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Set.univ`	—	`zero_add` `iUnion_Ico_add_zsmul`
`iUnion_Ioc_add_intCast` 📖	mathematical	—	`Set.iUnion` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Set.univ`	—	`zsmul_one` `Int.cast_add` `Int.cast_one` `iUnion_Ioc_add_zsmul` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`
`iUnion_Ioc_add_zsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Set.iUnion` `Set.Ioc` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Set.univ`	—	`Set.eq_univ_iff_forall` `Set.mem_iUnion` `sub_toIocDiv_zsmul_mem_Ioc` `lt_sub_iff_add_lt` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `add_smul` `one_smul` `add_assoc` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `sub_le_iff_le_add`
`iUnion_Ioc_intCast` 📖	mathematical	—	`Set.iUnion` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Set.univ`	—	`zero_add` `iUnion_Ioc_add_intCast`
`iUnion_Ioc_zsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Set.iUnion` `Set.Ioc` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Set.univ`	—	`zero_add` `iUnion_Ioc_add_zsmul`
`left_le_toIcoMod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Preorder.toLE` `toIcoMod`	—	`Set.mem_Ico` `toIcoMod_mem_Ico`
`left_lt_toIocMod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod`	—	`Set.mem_Ioc` `toIocMod_mem_Ioc`
`self_sub_toIcoDiv_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast` `toIcoDiv` `NonUnitalNonAssocRing.toAddCommGroup` `toIcoMod`	—	`zsmul_eq_mul` `self_sub_toIcoDiv_zsmul`
`self_sub_toIcoDiv_zsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul` `toIcoDiv` `toIcoMod`	—	—
`self_sub_toIcoMod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `toIcoMod` `SubNegMonoid.toZSMul` `toIcoDiv`	—	`toIcoMod.eq_1` `sub_sub_cancel`
`self_sub_toIcoMod_eq_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast` `toIcoDiv`	—	`self_sub_toIcoMod` `zsmul_eq_mul`
`self_sub_toIocDiv_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast` `toIocDiv` `NonUnitalNonAssocRing.toAddCommGroup` `toIocMod`	—	`zsmul_eq_mul` `self_sub_toIocDiv_zsmul`
`self_sub_toIocDiv_zsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul` `toIocDiv` `toIocMod`	—	—
`self_sub_toIocMod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `toIocMod` `SubNegMonoid.toZSMul` `toIocDiv`	—	`toIocMod.eq_1` `sub_sub_cancel`
`self_sub_toIocMod_eq_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast` `toIocDiv`	—	`self_sub_toIocMod` `zsmul_eq_mul`
`sub_toIcoDiv_zsmul_mem_Ico` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Set` `Set.instMembership` `Set.Ico` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul` `toIcoDiv`	—	`existsUnique_sub_zsmul_mem_Ico`
`sub_toIocDiv_zsmul_mem_Ioc` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Set` `Set.instMembership` `Set.Ioc` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul` `toIocDiv`	—	`existsUnique_sub_zsmul_mem_Ioc`
`toIcoDiv_add_intCast_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoDiv` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIcoDiv.congr_simp` `zsmul_eq_mul` `toIcoDiv_add_zsmul`
`toIcoDiv_add_intCast_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoDiv` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIcoDiv.congr_simp` `zsmul_eq_mul` `toIcoDiv_add_zsmul'`
`toIcoDiv_add_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`add_comm` `toIcoDiv_add_right`
`toIcoDiv_add_left'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`add_comm` `toIcoDiv_add_right'`
`toIcoDiv_add_natCast_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoDiv` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIcoDiv.congr_simp` `Int.cast_natCast` `toIcoDiv_add_intCast_mul`
`toIcoDiv_add_natCast_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoDiv` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIcoDiv.congr_simp` `Int.cast_natCast` `toIcoDiv_add_intCast_mul'`
`toIcoDiv_add_nsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIcoDiv.congr_simp` `Nat.cast_smul_eq_nsmul` `toIcoDiv_add_zsmul`
`toIcoDiv_add_nsmul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIcoDiv.congr_simp` `Nat.cast_smul_eq_nsmul` `toIcoDiv_add_zsmul'`
`toIcoDiv_add_ofNat_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoDiv` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	`toIcoDiv_add_natCast_mul`
`toIcoDiv_add_ofNat_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoDiv` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	`toIcoDiv_add_natCast_mul'`
`toIcoDiv_add_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`toIcoDiv.congr_simp` `one_zsmul` `toIcoDiv_add_zsmul`
`toIcoDiv_add_right'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`toIcoDiv.congr_simp` `one_zsmul` `toIcoDiv_add_zsmul'`
`toIcoDiv_add_zsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIcoDiv_eq_of_sub_zsmul_mem_Ico` `add_smul` `add_sub_add_right_eq_sub` `sub_toIcoDiv_zsmul_mem_Ico`
`toIcoDiv_add_zsmul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIcoDiv_eq_of_sub_zsmul_mem_Ico` `sub_smul` `sub_add` `add_right_comm` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `sub_toIcoDiv_zsmul_mem_Ico`
`toIcoDiv_apply_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv`	—	`toIcoDiv_eq_of_sub_zsmul_mem_Ico` `zero_smul` `sub_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `contravariant_lt_of_covariant_le`
`toIcoDiv_apply_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`toIcoDiv_eq_of_sub_zsmul_mem_Ico` `one_smul` `add_sub_cancel_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `contravariant_lt_of_covariant_le`
`toIcoDiv_eq_floor` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`toIcoDiv` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsStrictOrderedRing.toIsOrderedRing` `FloorRing.archimedean` `Int.floor` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`toIcoDiv_eq_of_sub_zsmul_mem_Ico` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `FloorRing.archimedean` `Set.mem_Ico` `zsmul_eq_mul` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `add_comm` `sub_right_comm` `sub_lt_iff_lt_add` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `Int.sub_floor_div_mul_nonneg` `Int.sub_floor_div_mul_lt`
`toIcoDiv_eq_iff` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `Set` `Set.instMembership` `Set.Ico` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul`	—	`ExistsUnique.choose_eq_iff` `existsUnique_sub_zsmul_mem_Ico`
`toIcoDiv_eq_of_sub_zsmul_mem_Ico` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Set.instMembership` `Set.Ico` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul`	`toIcoDiv`	—	`toIcoDiv_eq_iff`
`toIcoDiv_eq_sub` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIcoDiv_sub_eq_toIcoDiv_add` `zero_add`
`toIcoDiv_intCast_mul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoDiv` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIcoDiv.congr_simp` `zsmul_eq_mul` `toIcoDiv_zsmul_add`
`toIcoDiv_mul_sub_self` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast` `toIcoDiv` `NonUnitalNonAssocRing.toAddCommGroup` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `toIcoMod`	—	`zsmul_eq_mul` `toIcoDiv_zsmul_sub_self`
`toIcoDiv_mul_sub_toIcoMod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `toIcoDiv` `NonUnitalNonAssocRing.toAddCommGroup` `toIcoMod`	—	`add_comm` `toIcoMod_add_toIcoDiv_mul`
`toIcoDiv_natCast_mul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoDiv` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIcoDiv.congr_simp` `Int.cast_natCast` `toIcoDiv_intCast_mul_add`
`toIcoDiv_neg` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `NegZeroClass.toNeg` `toIocDiv`	—	`neg_eq_iff_eq_neg` `toIocDiv_eq_of_sub_zsmul_mem_Ioc` `sub_toIcoDiv_zsmul_mem_Ico` `neg_smul` `neg_neg` `neg_sub'` `neg_lt_neg_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `LE.le.trans_eq` `neg_le_neg_iff` `neg_add` `neg_add_cancel_right` `toIocDiv_add_right` `toIocDiv_sub_eq_toIocDiv_add'` `sub_eq_add_neg`
`toIcoDiv_neg'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `NegZeroClass.toNeg` `toIocDiv`	—	`toIcoDiv.congr_simp` `neg_neg` `toIocDiv.congr_simp` `toIcoDiv_neg`
`toIcoDiv_nsmul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIcoDiv.congr_simp` `Nat.cast_smul_eq_nsmul` `toIcoDiv_zsmul_add`
`toIcoDiv_ofNat_mul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoDiv` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	`toIcoDiv_natCast_mul_add`
`toIcoDiv_sub` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIcoDiv.congr_simp` `one_zsmul` `toIcoDiv_sub_zsmul`
`toIcoDiv_sub'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIcoDiv.congr_simp` `one_zsmul` `toIcoDiv_sub_zsmul'`
`toIcoDiv_sub_eq_toIcoDiv_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`toIcoDiv_eq_of_sub_zsmul_mem_Ico` `sub_right_comm` `Set.sub_mem_Ico_iff_left` `add_right_comm` `sub_toIcoDiv_zsmul_mem_Ico`
`toIcoDiv_sub_eq_toIcoDiv_add'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`sub_neg_eq_add` `toIcoDiv_sub_eq_toIcoDiv_add` `sub_eq_add_neg`
`toIcoDiv_sub_intCast_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoDiv` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast`	—	`toIcoDiv.congr_simp` `zsmul_eq_mul` `toIcoDiv_sub_zsmul`
`toIcoDiv_sub_intCast_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoDiv` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast`	—	`toIcoDiv.congr_simp` `zsmul_eq_mul` `toIcoDiv_sub_zsmul'`
`toIcoDiv_sub_natCast_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoDiv` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne`	—	`toIcoDiv.congr_simp` `Int.cast_natCast` `toIcoDiv_sub_intCast_mul`
`toIcoDiv_sub_natCast_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoDiv` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne`	—	`toIcoDiv.congr_simp` `Int.cast_natCast` `toIcoDiv_sub_intCast_mul'`
`toIcoDiv_sub_nsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid`	—	`toIcoDiv.congr_simp` `Nat.cast_smul_eq_nsmul` `toIcoDiv_sub_zsmul`
`toIcoDiv_sub_nsmul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid`	—	`toIcoDiv.congr_simp` `Nat.cast_smul_eq_nsmul` `toIcoDiv_sub_zsmul'`
`toIcoDiv_sub_ofNat_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoDiv` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`toIcoDiv_sub_natCast_mul`
`toIcoDiv_sub_ofNat_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoDiv` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`toIcoDiv_sub_natCast_mul'`
`toIcoDiv_sub_zsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul`	—	`sub_eq_add_neg` `neg_smul` `toIcoDiv_add_zsmul`
`toIcoDiv_sub_zsmul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul`	—	`sub_eq_add_neg` `neg_smul` `toIcoDiv_add_zsmul'` `sub_neg_eq_add`
`toIcoDiv_zero_one` 📖	mathematical	—	`toIcoDiv` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedRing` `FloorRing.archimedean` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `zero_lt_one'` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Ring.toSemiring` `Int.floor`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `FloorRing.archimedean` `zero_lt_one'` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `toIcoDiv_eq_floor` `sub_zero` `div_one`
`toIcoDiv_zsmul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`add_comm` `toIcoDiv_add_zsmul`
`toIcoDiv_zsmul_sub_self` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul` `toIcoDiv` `NegZeroClass.toNeg` `toIcoMod`	—	`toIcoMod.eq_1` `neg_sub`
`toIcoDiv_zsmul_sub_toIcoMod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `toIcoDiv` `toIcoMod`	—	`add_comm` `toIcoMod_add_toIcoDiv_zsmul`
`toIcoMod_add_intCast_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIcoMod.congr_simp` `zsmul_eq_mul` `toIcoMod_add_zsmul`
`toIcoMod_add_intCast_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIcoMod.congr_simp` `zsmul_eq_mul` `toIcoMod_add_zsmul'`
`toIcoMod_add_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`add_comm` `toIcoMod_add_right`
`toIcoMod_add_left'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`add_comm` `toIcoMod_add_right'`
`toIcoMod_add_natCast_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIcoMod.congr_simp` `Int.cast_natCast` `toIcoMod_add_intCast_mul`
`toIcoMod_add_natCast_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIcoMod.congr_simp` `Int.cast_natCast` `toIcoMod_add_intCast_mul'`
`toIcoMod_add_nsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIcoMod.congr_simp` `Nat.cast_smul_eq_nsmul` `toIcoMod_add_zsmul`
`toIcoMod_add_nsmul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIcoMod.congr_simp` `Nat.cast_smul_eq_nsmul` `toIcoMod_add_zsmul'`
`toIcoMod_add_ofNat_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	`toIcoMod.congr_simp` `Int.cast_natCast` `toIcoMod_add_intCast_mul`
`toIcoMod_add_ofNat_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	`toIcoMod_add_natCast_mul'`
`toIcoMod_add_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`toIcoMod.congr_simp` `one_zsmul` `toIcoMod_add_zsmul`
`toIcoMod_add_right'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`toIcoMod.congr_simp` `one_zsmul` `toIcoMod_add_zsmul'`
`toIcoMod_add_right_eq_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIcoDiv_sub_eq_toIcoDiv_add'` `sub_add_eq_add_sub`
`toIcoMod_add_toIcoDiv_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toMul` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `toIcoDiv`	—	`zsmul_eq_mul` `toIcoMod_add_toIcoDiv_zsmul`
`toIcoMod_add_toIcoDiv_zsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `toIcoMod` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `toIcoDiv`	—	`toIcoMod.eq_1` `sub_add_cancel`
`toIcoMod_add_toIocMod_zero` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `toIcoMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `toIocMod`	—	`toIcoMod_zero_sub_comm` `sub_add_cancel`
`toIcoMod_add_zsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIcoMod.eq_1` `toIcoDiv_add_zsmul` `add_smul` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Tactic.Abel.zero_termg`
`toIcoMod_add_zsmul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIcoDiv_add_zsmul'` `sub_smul` `sub_add`
`toIcoMod_apply_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod`	—	`toIcoMod_eq_iff` `Set.left_mem_Ico` `lt_add_of_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `zero_smul` `add_zero`
`toIcoMod_apply_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`toIcoMod_eq_iff` `Set.left_mem_Ico` `lt_add_of_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `one_smul`
`toIcoMod_eq_add_fract_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`toIcoMod` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsStrictOrderedRing.toIsOrderedRing` `FloorRing.archimedean` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `Int.fract` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `FloorRing.archimedean` `toIcoMod.eq_1` `toIcoDiv_eq_floor` `Int.fract.eq_1` `zsmul_eq_mul` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add`
`toIcoMod_eq_fract_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`toIcoMod` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsStrictOrderedRing.toIsOrderedRing` `FloorRing.archimedean` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Int.fract` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `FloorRing.archimedean` `toIcoMod_eq_add_fract_mul` `sub_zero` `zero_add`
`toIcoMod_eq_iff` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `Set` `Set.instMembership` `Set.Ico` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIcoMod_mem_Ico` `toIcoMod_add_toIcoDiv_zsmul` `toIcoDiv_eq_of_sub_zsmul_mem_Ico` `toIcoMod.eq_1`
`toIcoMod_eq_self` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `Set` `Set.instMembership` `Set.Ico` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`toIcoMod_eq_iff` `zero_smul` `add_zero`
`toIcoMod_eq_sub` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIcoMod_sub_eq_sub` `zero_add` `sub_add_cancel`
`toIcoMod_eq_toIcoMod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul`	—	`toIcoMod_add_toIcoDiv_zsmul` `sub_smul` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Tactic.Abel.zero_termg` `sub_eq_iff_eq_add` `toIcoMod_zsmul_add`
`toIcoMod_inj` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `AddCommGroup.ModEq` `AddCommGroup.toAddCommMonoid`	—	`toIcoMod_eq_toIcoMod` `AddCommGroup.modEq_iff_zsmul'`
`toIcoMod_intCast_mul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIcoMod.congr_simp` `zsmul_eq_mul` `toIcoMod_zsmul_add`
`toIcoMod_intCast_mul_add'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`add_comm` `toIcoMod_add_intCast_mul'`
`toIcoMod_le_toIocMod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Preorder.toLE` `toIcoMod` `toIocMod`	—	`toIcoMod.eq_1` `toIocMod.eq_1` `sub_le_sub_iff_left` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `zsmul_left_mono` `LT.lt.le` `WCovBy.le` `toIocDiv_wcovBy_toIcoDiv`
`toIcoMod_lt_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`Set.mem_Ico` `toIcoMod_mem_Ico`
`toIcoMod_mem_Ico` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Set` `Set.instMembership` `Set.Ico` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `toIcoMod`	—	`sub_toIcoDiv_zsmul_mem_Ico`
`toIcoMod_mem_Ico'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Set` `Set.instMembership` `Set.Ico` `toIcoMod`	—	`zero_add` `toIcoMod_mem_Ico`
`toIcoMod_natCast_mul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIcoMod.congr_simp` `Int.cast_natCast` `toIcoMod_intCast_mul_add`
`toIcoMod_natCast_mul_add'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIcoMod.congr_simp` `Int.cast_natCast` `toIcoMod_intCast_mul_add'`
`toIcoMod_neg` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `NegZeroClass.toNeg` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `toIocMod`	—	`toIcoDiv_neg` `neg_smul` `add_smul` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.subst_into_smulg` `Mathlib.Tactic.Abel.term_smulg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.zero_smulg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Abel.const_add_termg` `add_zero`
`toIcoMod_neg'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `NegZeroClass.toNeg` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `toIocMod`	—	`toIcoMod.congr_simp` `neg_neg` `toIocMod.congr_simp` `toIcoMod_neg`
`toIcoMod_nsmul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIcoMod.congr_simp` `Nat.cast_smul_eq_nsmul` `toIcoMod_zsmul_add`
`toIcoMod_nsmul_add'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIcoMod.congr_simp` `Nat.cast_smul_eq_nsmul` `toIcoMod_zsmul_add'`
`toIcoMod_ofNat_mul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	`toIcoMod_natCast_mul_add`
`toIcoMod_ofNat_mul_add'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	`toIcoMod_natCast_mul_add'`
`toIcoMod_periodic` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Function.Periodic` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `toIcoMod`	—	`toIcoMod_add_right`
`toIcoMod_sub` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIcoMod.congr_simp` `one_zsmul` `toIcoMod_sub_zsmul`
`toIcoMod_sub'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIcoMod.congr_simp` `one_zsmul` `toIcoMod_sub_zsmul'`
`toIcoMod_sub_eq_sub` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`toIcoDiv_sub_eq_toIcoDiv_add` `sub_right_comm`
`toIcoMod_sub_intCast_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast`	—	`toIcoMod.congr_simp` `zsmul_eq_mul` `toIcoMod_sub_zsmul`
`toIcoMod_sub_intCast_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast`	—	`toIcoMod.congr_simp` `zsmul_eq_mul` `toIcoMod_sub_zsmul'`
`toIcoMod_sub_natCast_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne`	—	`toIcoMod.congr_simp` `Int.cast_natCast` `toIcoMod_sub_intCast_mul`
`toIcoMod_sub_natCast_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne`	—	`toIcoMod.congr_simp` `Int.cast_natCast` `toIcoMod_sub_intCast_mul'`
`toIcoMod_sub_nsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid`	—	`toIcoMod.congr_simp` `Nat.cast_smul_eq_nsmul` `toIcoMod_sub_zsmul`
`toIcoMod_sub_nsmul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid`	—	`toIcoMod.congr_simp` `Nat.cast_smul_eq_nsmul` `toIcoMod_sub_zsmul'`
`toIcoMod_sub_ofNat_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`toIcoMod_sub_natCast_mul`
`toIcoMod_sub_ofNat_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`toIcoMod_sub_natCast_mul'`
`toIcoMod_sub_self` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `toIcoMod` `SubNegMonoid.toZSMul` `toIcoDiv`	—	`toIcoMod.eq_1` `sub_sub_cancel_left` `neg_smul`
`toIcoMod_sub_self_eq_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `toIcoMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddGroupWithOne.toIntCast` `toIcoDiv`	—	`toIcoMod_sub_self` `neg_smul` `zsmul_eq_mul` `neg_mul`
`toIcoMod_sub_zsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul`	—	`sub_eq_add_neg` `neg_smul` `toIcoMod_add_zsmul`
`toIcoMod_sub_zsmul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul`	—	`toIcoMod.congr_simp` `sub_eq_add_neg` `toIcoMod_add_zsmul'`
`toIcoMod_toIcoMod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod`	—	`toIcoMod_eq_toIcoMod` `self_sub_toIcoMod`
`toIcoMod_toIocMod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `toIocMod`	—	`toIcoMod_eq_toIcoMod` `self_sub_toIocMod`
`toIcoMod_zero_one` 📖	mathematical	—	`toIcoMod` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedRing` `FloorRing.archimedean` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `zero_lt_one'` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Ring.toSemiring` `Int.fract`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `FloorRing.archimedean` `zero_lt_one'` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `toIcoMod_eq_add_fract_mul` `sub_zero` `div_one` `mul_one` `zero_add`
`toIcoMod_zero_sub_comm` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `toIocMod`	—	`neg_sub` `toIcoMod_neg` `neg_zero`
`toIcoMod_zsmul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`add_comm` `toIcoMod_add_zsmul`
`toIcoMod_zsmul_add'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIcoMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`add_comm` `toIcoMod_add_zsmul'`
`toIocDiv_add_intCast_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocDiv` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIocDiv.congr_simp` `zsmul_eq_mul` `toIocDiv_add_zsmul`
`toIocDiv_add_intCast_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocDiv` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIocDiv.congr_simp` `zsmul_eq_mul` `toIocDiv_add_zsmul'`
`toIocDiv_add_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`add_comm` `toIocDiv_add_right`
`toIocDiv_add_left'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`add_comm` `toIocDiv_add_right'`
`toIocDiv_add_natCast_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocDiv` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIocDiv.congr_simp` `Int.cast_natCast` `toIocDiv_add_intCast_mul`
`toIocDiv_add_natCast_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocDiv` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIocDiv.congr_simp` `Int.cast_natCast` `toIocDiv_add_intCast_mul'`
`toIocDiv_add_nsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIocDiv.congr_simp` `Nat.cast_smul_eq_nsmul` `toIocDiv_add_zsmul`
`toIocDiv_add_nsmul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIocDiv.congr_simp` `Nat.cast_smul_eq_nsmul` `toIocDiv_add_zsmul'`
`toIocDiv_add_ofNat_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocDiv` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	`toIocDiv_add_natCast_mul`
`toIocDiv_add_ofNat_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocDiv` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	`toIocDiv_add_natCast_mul'`
`toIocDiv_add_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`toIocDiv.congr_simp` `one_zsmul` `toIocDiv_add_zsmul`
`toIocDiv_add_right'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`toIocDiv.congr_simp` `one_zsmul` `toIocDiv_add_zsmul'`
`toIocDiv_add_zsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIocDiv_eq_of_sub_zsmul_mem_Ioc` `add_smul` `add_sub_add_right_eq_sub` `sub_toIocDiv_zsmul_mem_Ioc`
`toIocDiv_add_zsmul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIocDiv_eq_of_sub_zsmul_mem_Ioc` `sub_smul` `sub_add` `add_right_comm` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `sub_toIocDiv_zsmul_mem_Ioc`
`toIocDiv_apply_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv`	—	`toIocDiv_eq_of_sub_zsmul_mem_Ioc` `neg_smul` `one_smul` `sub_neg_eq_add` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `contravariant_lt_of_covariant_le`
`toIocDiv_apply_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`toIocDiv_eq_of_sub_zsmul_mem_Ioc` `zero_smul` `sub_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `contravariant_lt_of_covariant_le`
`toIocDiv_eq_iff` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `Set` `Set.instMembership` `Set.Ioc` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul`	—	`ExistsUnique.choose_eq_iff` `existsUnique_sub_zsmul_mem_Ioc`
`toIocDiv_eq_neg_floor` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`toIocDiv` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsStrictOrderedRing.toIsOrderedRing` `FloorRing.archimedean` `Int.floor` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`toIocDiv_eq_of_sub_zsmul_mem_Ioc` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `FloorRing.archimedean` `Set.mem_Ioc` `zsmul_eq_mul` `Int.cast_neg` `neg_mul` `sub_neg_eq_add` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `sub_add_eq_sub_sub` `add_lt_add_iff_right` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `add_assoc` `add_comm` `sub_lt_iff_lt_add` `Int.sub_floor_div_mul_lt` `Int.sub_floor_div_mul_nonneg`
`toIocDiv_eq_of_sub_zsmul_mem_Ioc` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set` `Set.instMembership` `Set.Ioc` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul`	`toIocDiv`	—	`toIocDiv_eq_iff`
`toIocDiv_eq_sub` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIocDiv_sub_eq_toIocDiv_add` `zero_add`
`toIocDiv_intCast_mul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocDiv` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIocDiv.congr_simp` `zsmul_eq_mul` `toIocDiv_zsmul_add`
`toIocDiv_mul_sub_self` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast` `toIocDiv` `NonUnitalNonAssocRing.toAddCommGroup` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `toIocMod`	—	`zsmul_eq_mul` `toIocDiv_zsmul_sub_self`
`toIocDiv_mul_sub_toIocMod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `toIocDiv` `NonUnitalNonAssocRing.toAddCommGroup` `toIocMod`	—	`add_comm` `toIocMod_add_toIocDiv_mul`
`toIocDiv_natCast_mul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocDiv` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIocDiv.congr_simp` `Int.cast_natCast` `toIocDiv_intCast_mul_add`
`toIocDiv_neg` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `NegZeroClass.toNeg` `toIcoDiv`	—	`neg_neg` `toIcoDiv_neg` `neg_add'` `add_sub_cancel_right`
`toIocDiv_neg'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `NegZeroClass.toNeg` `toIcoDiv`	—	`toIocDiv.congr_simp` `neg_neg` `toIcoDiv.congr_simp` `toIocDiv_neg`
`toIocDiv_nsmul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIocDiv.congr_simp` `Nat.cast_smul_eq_nsmul` `toIocDiv_zsmul_add`
`toIocDiv_ofNat_mul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocDiv` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	`toIocDiv_natCast_mul_add`
`toIocDiv_sub` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIocDiv.congr_simp` `one_zsmul` `toIocDiv_sub_zsmul`
`toIocDiv_sub'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIocDiv.congr_simp` `one_zsmul` `toIocDiv_sub_zsmul'`
`toIocDiv_sub_eq_toIocDiv_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`toIocDiv_eq_of_sub_zsmul_mem_Ioc` `sub_right_comm` `Set.sub_mem_Ioc_iff_left` `add_right_comm` `sub_toIocDiv_zsmul_mem_Ioc`
`toIocDiv_sub_eq_toIocDiv_add'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`sub_neg_eq_add` `toIocDiv_sub_eq_toIocDiv_add` `sub_eq_add_neg`
`toIocDiv_sub_intCast_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocDiv` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast`	—	`toIocDiv.congr_simp` `zsmul_eq_mul` `toIocDiv_sub_zsmul`
`toIocDiv_sub_intCast_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocDiv` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast`	—	`toIocDiv.congr_simp` `zsmul_eq_mul` `toIocDiv_sub_zsmul'`
`toIocDiv_sub_natCast_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocDiv` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne`	—	`toIocDiv.congr_simp` `Int.cast_natCast` `toIocDiv_sub_intCast_mul`
`toIocDiv_sub_natCast_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocDiv` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne`	—	`toIocDiv.congr_simp` `Int.cast_natCast` `toIocDiv_sub_intCast_mul'`
`toIocDiv_sub_nsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid`	—	`toIocDiv.congr_simp` `Nat.cast_smul_eq_nsmul` `toIocDiv_sub_zsmul`
`toIocDiv_sub_nsmul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid`	—	`toIocDiv.congr_simp` `Nat.cast_smul_eq_nsmul` `toIocDiv_sub_zsmul'`
`toIocDiv_sub_ofNat_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocDiv` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`toIocDiv_sub_natCast_mul`
`toIocDiv_sub_ofNat_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocDiv` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`toIocDiv_sub_natCast_mul'`
`toIocDiv_sub_zsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul`	—	`sub_eq_add_neg` `neg_smul` `toIocDiv_add_zsmul`
`toIocDiv_sub_zsmul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul`	—	`sub_eq_add_neg` `neg_smul` `toIocDiv_add_zsmul'` `sub_neg_eq_add`
`toIocDiv_wcovBy_toIcoDiv` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`WCovBy` `instLatticeInt` `toIocDiv` `toIcoDiv`	—	`AddCommGroup.not_modEq_iff_toIcoDiv_eq_toIocDiv` `AddCommGroup.modEq_iff_toIcoDiv_eq_toIocDiv_add_one` `em'` `wcovBy_iff_eq_or_covBy` `Order.succ_eq_iff_covBy` `instNoMaxOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `Int.instNontrivial`
`toIocDiv_zsmul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocDiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`add_comm` `toIocDiv_add_zsmul`
`toIocDiv_zsmul_sub_self` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul` `toIocDiv` `NegZeroClass.toNeg` `toIocMod`	—	`toIocMod.eq_1` `neg_sub`
`toIocDiv_zsmul_sub_toIocMod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `toIocDiv` `toIocMod`	—	`add_comm` `toIocMod_add_toIocDiv_zsmul`
`toIocMod_add_intCast_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIocMod.congr_simp` `zsmul_eq_mul` `toIocMod_add_zsmul`
`toIocMod_add_intCast_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIocMod.congr_simp` `zsmul_eq_mul` `toIocMod_add_zsmul'`
`toIocMod_add_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`add_comm` `toIocMod_add_right`
`toIocMod_add_left'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`add_comm` `toIocMod_add_right'`
`toIocMod_add_natCast_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIocMod.congr_simp` `Int.cast_natCast` `toIocMod_add_intCast_mul`
`toIocMod_add_natCast_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIocMod.congr_simp` `Int.cast_natCast` `toIocMod_add_intCast_mul'`
`toIocMod_add_nsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIocMod.congr_simp` `Nat.cast_smul_eq_nsmul` `toIocMod_add_zsmul`
`toIocMod_add_nsmul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIocMod.congr_simp` `Nat.cast_smul_eq_nsmul` `toIocMod_add_zsmul'`
`toIocMod_add_ofNat_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	`toIocMod_add_natCast_mul`
`toIocMod_add_ofNat_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	`toIocMod_add_natCast_mul'`
`toIocMod_add_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`toIocMod.congr_simp` `one_zsmul` `toIocMod_add_zsmul`
`toIocMod_add_right'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`toIocMod.congr_simp` `one_zsmul` `toIocMod_add_zsmul'`
`toIocMod_add_right_eq_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIocDiv_sub_eq_toIocDiv_add'` `sub_add_eq_add_sub`
`toIocMod_add_toIcoMod_zero` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `toIocMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `toIcoMod`	—	`add_comm` `toIcoMod_add_toIocMod_zero`
`toIocMod_add_toIocDiv_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toMul` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `toIocDiv`	—	`zsmul_eq_mul` `toIocMod_add_toIocDiv_zsmul`
`toIocMod_add_toIocDiv_zsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `toIocMod` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `toIocDiv`	—	`toIocMod.eq_1` `sub_add_cancel`
`toIocMod_add_zsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIocMod.eq_1` `toIocDiv_add_zsmul` `add_smul` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Tactic.Abel.zero_termg`
`toIocMod_add_zsmul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIocDiv_add_zsmul'` `sub_smul` `sub_add`
`toIocMod_apply_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`toIocMod_eq_iff` `Set.right_mem_Ioc` `lt_add_of_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `neg_smul` `one_smul` `add_neg_cancel_right`
`toIocMod_apply_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`toIocMod_eq_iff` `Set.right_mem_Ioc` `lt_add_of_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `zero_smul` `add_zero`
`toIocMod_eq_iff` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `Set` `Set.instMembership` `Set.Ioc` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIocMod_mem_Ioc` `toIocMod_add_toIocDiv_zsmul` `toIocDiv_eq_of_sub_zsmul_mem_Ioc` `toIocMod.eq_1`
`toIocMod_eq_self` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `Set` `Set.instMembership` `Set.Ioc` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`toIocMod_eq_iff` `zero_smul` `add_zero`
`toIocMod_eq_sub` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIocMod_sub_eq_sub` `zero_add` `sub_add_cancel`
`toIocMod_eq_sub_fract_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`toIocMod` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsStrictOrderedRing.toIsOrderedRing` `FloorRing.archimedean` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `Int.fract` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `FloorRing.archimedean` `toIocMod.eq_1` `toIocDiv_eq_neg_floor` `Int.fract.eq_1` `neg_smul` `zsmul_eq_mul` `sub_neg_eq_add` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add`
`toIocMod_eq_toIocMod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul`	—	`toIocMod_add_toIocDiv_zsmul` `sub_smul` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Tactic.Abel.zero_termg` `sub_eq_iff_eq_add` `toIocMod_zsmul_add`
`toIocMod_intCast_mul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`add_comm` `toIocMod_add_intCast_mul`
`toIocMod_intCast_mul_add'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`add_comm` `toIocMod_add_intCast_mul'`
`toIocMod_le_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Preorder.toLE` `toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`Set.mem_Ioc` `toIocMod_mem_Ioc`
`toIocMod_le_toIcoMod_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Preorder.toLE` `toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `toIcoMod`	—	`toIcoMod.eq_1` `toIocMod.eq_1` `sub_add` `sub_le_sub_iff_left` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `sub_le_iff_le_add` `add_one_zsmul` `StrictMono.le_iff_le` `zsmul_left_strictMono` `WCovBy.le_succ` `toIocDiv_wcovBy_toIcoDiv`
`toIocMod_mem_Ioc` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Set` `Set.instMembership` `Set.Ioc` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `toIocMod`	—	`sub_toIocDiv_zsmul_mem_Ioc`
`toIocMod_natCast_mul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIocMod.congr_simp` `Int.cast_natCast` `toIocMod_intCast_mul_add`
`toIocMod_natCast_mul_add'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne`	—	`toIocMod.congr_simp` `Int.cast_natCast` `toIocMod_intCast_mul_add'`
`toIocMod_neg` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `NegZeroClass.toNeg` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `toIcoMod`	—	`toIocDiv_neg` `neg_smul` `add_smul` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.subst_into_smulg` `Mathlib.Tactic.Abel.term_smulg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.zero_smulg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Abel.const_add_termg` `add_zero`
`toIocMod_neg'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `NegZeroClass.toNeg` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `toIcoMod`	—	`toIocMod.congr_simp` `neg_neg` `toIcoMod.congr_simp` `toIocMod_neg`
`toIocMod_nsmul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIocMod.congr_simp` `Nat.cast_smul_eq_nsmul` `toIocMod_zsmul_add`
`toIocMod_nsmul_add'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIocMod.congr_simp` `Nat.cast_smul_eq_nsmul` `toIocMod_zsmul_add'`
`toIocMod_ofNat_mul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	`toIocMod_natCast_mul_add`
`toIocMod_ofNat_mul_add'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	`toIocMod_natCast_mul_add'`
`toIocMod_periodic` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Function.Periodic` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `toIocMod`	—	`toIocMod_add_right`
`toIocMod_sub` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIocMod.congr_simp` `one_zsmul` `toIocMod_sub_zsmul`
`toIocMod_sub'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`toIocMod.congr_simp` `one_zsmul` `toIocMod_sub_zsmul'`
`toIocMod_sub_eq_sub` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`toIocDiv_sub_eq_toIocDiv_add` `sub_right_comm`
`toIocMod_sub_intCast_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast`	—	`toIocMod.congr_simp` `zsmul_eq_mul` `toIocMod_sub_zsmul`
`toIocMod_sub_intCast_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast`	—	`toIocMod.congr_simp` `zsmul_eq_mul` `toIocMod_sub_zsmul'`
`toIocMod_sub_natCast_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne`	—	`toIocMod.congr_simp` `Int.cast_natCast` `toIocMod_sub_intCast_mul`
`toIocMod_sub_natCast_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne`	—	`toIocMod.congr_simp` `Int.cast_natCast` `toIocMod_sub_intCast_mul'`
`toIocMod_sub_nsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid`	—	`toIocMod.congr_simp` `Nat.cast_smul_eq_nsmul` `toIocMod_sub_zsmul`
`toIocMod_sub_nsmul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid`	—	`toIocMod.congr_simp` `Nat.cast_smul_eq_nsmul` `toIocMod_sub_zsmul'`
`toIocMod_sub_ofNat_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`toIocMod_sub_natCast_mul`
`toIocMod_sub_ofNat_mul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`toIocMod_sub_natCast_mul'`
`toIocMod_sub_self` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `toIocMod` `SubNegMonoid.toZSMul` `toIocDiv`	—	`toIocMod.eq_1` `sub_sub_cancel_left` `neg_smul`
`toIocMod_sub_self_eq_mul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `toIocMod` `NonUnitalNonAssocRing.toAddCommGroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddGroupWithOne.toIntCast` `toIocDiv`	—	`toIocMod_sub_self` `neg_smul` `zsmul_eq_mul` `neg_mul`
`toIocMod_sub_zsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul`	—	`sub_eq_add_neg` `neg_smul` `toIocMod_add_zsmul`
`toIocMod_sub_zsmul'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SubNegMonoid.toZSMul`	—	`toIocMod.congr_simp` `sub_eq_add_neg` `toIocMod_add_zsmul'`
`toIocMod_toIcoMod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `toIcoMod`	—	`toIocMod_eq_toIocMod` `self_sub_toIcoMod`
`toIocMod_toIocMod` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod`	—	`toIocMod_eq_toIocMod` `self_sub_toIocMod`
`toIocMod_zero_sub_comm` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `toIcoMod`	—	`neg_sub` `toIocMod_neg` `neg_zero`
`toIocMod_zsmul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`add_comm` `toIocMod_add_zsmul`
`toIocMod_zsmul_add'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`toIocMod` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`add_comm` `toIocMod_add_zsmul'`

---

← Back to Index