Interval

📁 Source: Mathlib/Algebra/Order/Group/Pointwise/Interval.lean

Statistics

Metric	Count
Definitions	0
Theorems `Icc_add_Icc`, `Icc_add_Icc_subset`, `Icc_add_Ico_subset`, `Icc_mul_Icc`, `Icc_mul_Icc_subset'`, `Icc_mul_Ico_subset'`, `Ici_add_Ici_eq`, `Ici_add_Ici_subset`, `Ici_add_Ioi_subset`, `Ici_mul_Ici_eq`, `Ici_mul_Ici_subset'`, `Ici_mul_Ioi_subset'`, `Ici_nsmul_eq`, `Ici_one_eq_univ`, `Ici_pow_eq`, `Ici_zero_eq_univ`, `Ico_add_Icc_subset`, `Ico_add_Ioc_subset`, `Ico_mul_Icc_subset'`, `Ico_mul_Ioc_subset'`, `Iic_add_Iic_subset`, `Iic_add_Iio_subset`, `Iic_add_bij`, `Iic_mul_Iic_subset'`, `Iic_mul_Iio_subset'`, `Iic_mul_bij`, `Iio_add_Iic_subset`, `Iio_add_bij`, `Iio_mul_Iic_subset'`, `Iio_mul_bij`, `Ioc_add_Ico_subset`, `Ioc_mul_Ico_subset'`, `Ioi_add_Ici_subset`, `Ioi_mul_Ici_subset'`, `abs_sub_le_of_uIcc_subset_uIcc`, `abs_sub_left_of_mem_uIcc`, `abs_sub_right_of_mem_uIcc`, `image_add_const_Iic`, `image_add_const_Iio`, `image_add_const_uIcc`, `image_affine_Icc'`, `image_affine_Ico`, `image_affine_Ioc`, `image_affine_Ioo`, `image_const_add_Iic`, `image_const_add_Iio`, `image_const_add_uIcc`, `image_const_div_Icc`, `image_const_div_Ici`, `image_const_div_Ico`, `image_const_div_Iic`, `image_const_div_Iio`, `image_const_div_Ioc`, `image_const_div_Ioi`, `image_const_div_Ioo`, `image_const_mul_Iic`, `image_const_mul_Iio`, `image_const_mul_Ioi_zero`, `image_const_mul_uIcc`, `image_const_sub_Icc`, `image_const_sub_Ici`, `image_const_sub_Ico`, `image_const_sub_Iic`, `image_const_sub_Iio`, `image_const_sub_Ioc`, `image_const_sub_Ioi`, `image_const_sub_Ioo`, `image_const_sub_uIcc`, `image_div_const_Icc`, `image_div_const_Ici`, `image_div_const_Ico`, `image_div_const_Iic`, `image_div_const_Iio`, `image_div_const_Ioc`, `image_div_const_Ioi`, `image_div_const_Ioo`, `image_div_const_uIcc`, `image_inv_Icc`, `image_inv_Ici`, `image_inv_Ico`, `image_inv_Iic`, `image_inv_Iio`, `image_inv_Ioc`, `image_inv_Ioi`, `image_inv_Ioo`, `image_mul_const_Iic`, `image_mul_const_Iio`, `image_mul_const_uIcc`, `image_mul_left_Icc`, `image_mul_left_Icc'`, `image_mul_left_Ici`, `image_mul_left_Ico`, `image_mul_left_Iic`, `image_mul_left_Iio`, `image_mul_left_Ioc`, `image_mul_left_Ioi`, `image_mul_left_Ioo`, `image_mul_right_Icc`, `image_mul_right_Icc'`, `image_mul_right_Ico`, `image_mul_right_Ioc`, `image_mul_right_Ioo`, `image_neg_Icc`, `image_neg_Ici`, `image_neg_Ico`, `image_neg_Iic`, `image_neg_Iio`, `image_neg_Ioc`, `image_neg_Ioi`, `image_neg_Ioo`, `image_neg_uIcc`, `image_sub_const_Icc`, `image_sub_const_Ici`, `image_sub_const_Ico`, `image_sub_const_Iic`, `image_sub_const_Iio`, `image_sub_const_Ioc`, `image_sub_const_Ioi`, `image_sub_const_Ioo`, `image_sub_const_uIcc`, `inv_Icc`, `inv_Ici`, `inv_Ico`, `inv_Iic`, `inv_Iio`, `inv_Iio₀`, `inv_Ioc`, `inv_Ioi`, `inv_Ioi₀`, `inv_Ioo`, `inv_Ioo_0_left`, `inv_Ioo_0_right`, `inv_uIcc`, `neg_Icc`, `neg_Ici`, `neg_Ico`, `neg_Iic`, `neg_Iio`, `neg_Ioc`, `neg_Ioi`, `neg_Ioo`, `neg_uIcc`, `preimage_add_const_Icc`, `preimage_add_const_Ici`, `preimage_add_const_Ico`, `preimage_add_const_Iic`, `preimage_add_const_Iio`, `preimage_add_const_Ioc`, `preimage_add_const_Ioi`, `preimage_add_const_Ioo`, `preimage_add_const_uIcc`, `preimage_const_add_Icc`, `preimage_const_add_Ici`, `preimage_const_add_Ico`, `preimage_const_add_Iic`, `preimage_const_add_Iio`, `preimage_const_add_Ioc`, `preimage_const_add_Ioi`, `preimage_const_add_Ioo`, `preimage_const_add_uIcc`, `preimage_const_div_Icc`, `preimage_const_div_Ici`, `preimage_const_div_Ico`, `preimage_const_div_Iic`, `preimage_const_div_Iio`, `preimage_const_div_Ioc`, `preimage_const_div_Ioi`, `preimage_const_div_Ioo`, `preimage_const_mul_Icc`, `preimage_const_mul_Icc_of_neg`, `preimage_const_mul_Icc₀`, `preimage_const_mul_Ici`, `preimage_const_mul_Ici_of_neg`, `preimage_const_mul_Ici₀`, `preimage_const_mul_Ico`, `preimage_const_mul_Ico_of_neg`, `preimage_const_mul_Ico₀`, `preimage_const_mul_Iic`, `preimage_const_mul_Iic_of_neg`, `preimage_const_mul_Iic₀`, `preimage_const_mul_Iio`, `preimage_const_mul_Iio_of_neg`, `preimage_const_mul_Iio₀`, `preimage_const_mul_Ioc`, `preimage_const_mul_Ioc_of_neg`, `preimage_const_mul_Ioc₀`, `preimage_const_mul_Ioi`, `preimage_const_mul_Ioi_of_neg`, `preimage_const_mul_Ioi_or_Iio`, `preimage_const_mul_Ioi₀`, `preimage_const_mul_Ioo`, `preimage_const_mul_Ioo_of_neg`, `preimage_const_mul_Ioo₀`, `preimage_const_mul_uIcc`, `preimage_const_sub_Icc`, `preimage_const_sub_Ici`, `preimage_const_sub_Ico`, `preimage_const_sub_Iic`, `preimage_const_sub_Iio`, `preimage_const_sub_Ioc`, `preimage_const_sub_Ioi`, `preimage_const_sub_Ioo`, `preimage_const_sub_uIcc`, `preimage_div_const_Icc`, `preimage_div_const_Ici`, `preimage_div_const_Ico`, `preimage_div_const_Iic`, `preimage_div_const_Iio`, `preimage_div_const_Ioc`, `preimage_div_const_Ioi`, `preimage_div_const_Ioo`, `preimage_div_const_uIcc`, `preimage_mul_const_Icc`, `preimage_mul_const_Icc_of_neg`, `preimage_mul_const_Icc₀`, `preimage_mul_const_Ici`, `preimage_mul_const_Ici_of_neg`, `preimage_mul_const_Ici₀`, `preimage_mul_const_Ico`, `preimage_mul_const_Ico_of_neg`, `preimage_mul_const_Ico₀`, `preimage_mul_const_Iic`, `preimage_mul_const_Iic_of_neg`, `preimage_mul_const_Iic₀`, `preimage_mul_const_Iio`, `preimage_mul_const_Iio_of_neg`, `preimage_mul_const_Iio₀`, `preimage_mul_const_Ioc`, `preimage_mul_const_Ioc_of_neg`, `preimage_mul_const_Ioc₀`, `preimage_mul_const_Ioi`, `preimage_mul_const_Ioi_of_neg`, `preimage_mul_const_Ioi₀`, `preimage_mul_const_Ioo`, `preimage_mul_const_Ioo_of_neg`, `preimage_mul_const_Ioo₀`, `preimage_mul_const_uIcc`, `preimage_sub_const_Icc`, `preimage_sub_const_Ici`, `preimage_sub_const_Ico`, `preimage_sub_const_Iic`, `preimage_sub_const_Iio`, `preimage_sub_const_Ioc`, `preimage_sub_const_Ioi`, `preimage_sub_const_Ioo`, `preimage_sub_const_uIcc`, `smul_Icc`, `vadd_Icc`	248
Total	248

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_add_Icc` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set` `add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Icc`	—	`HasSubset.Subset.antisymm` `instAntisymmSubset` `Icc_add_Icc_subset` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `le_total` `exists_nonneg_add_of_le` `le_add_of_nonneg_right` `add_le_add_iff_right` `contravariant_swap_add_of_contravariant_add` `add_right_comm` `left_mem_Icc` `right_mem_Icc` `add_le_add_iff_left` `add_assoc`
`Icc_add_Icc_subset` 📖	mathematical	—	`Set` `instHasSubset` `add` `Icc`	—	`add_le_add`
`Icc_add_Ico_subset` 📖	mathematical	—	`Set` `instHasSubset` `add` `Icc` `PartialOrder.toPreorder` `Ico`	—	`addLeftMono_of_addLeftStrictMono` `addRightMono_of_addRightStrictMono` `add_le_add` `add_lt_add_of_le_of_lt`
`Icc_mul_Icc` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Icc`	—	`HasSubset.Subset.antisymm` `instAntisymmSubset` `Icc_mul_Icc_subset'` `IsOrderedMonoid.toMulLeftMono` `covariant_swap_mul_of_covariant_mul` `le_total` `exists_one_le_mul_of_le` `le_mul_of_one_le_right'` `mul_le_mul_iff_right` `contravariant_swap_mul_of_contravariant_mul` `mul_right_comm` `left_mem_Icc` `right_mem_Icc` `mul_le_mul_iff_left` `mul_assoc`
`Icc_mul_Icc_subset'` 📖	mathematical	—	`Set` `instHasSubset` `mul` `Icc`	—	`mul_le_mul'`
`Icc_mul_Ico_subset'` 📖	mathematical	—	`Set` `instHasSubset` `mul` `Icc` `PartialOrder.toPreorder` `Ico`	—	`mulLeftMono_of_mulLeftStrictMono` `mulRightMono_of_mulRightStrictMono` `mul_le_mul'` `mul_lt_mul_of_le_of_lt`
`Ici_add_Ici_eq` 📖	mathematical	—	`Set` `add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Ici`	—	`Subset.antisymm` `Ici_add_Ici_subset` `CanonicallyOrderedAdd.toAddLeftMono` `mem_add` `mem_Ici` `le_refl` `ExistsAddOfLE.exists_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `self_le_add_right` `add_assoc` `subset_def`
`Ici_add_Ici_subset` 📖	mathematical	—	`Set` `instHasSubset` `add` `Ici`	—	`add_le_add`
`Ici_add_Ioi_subset` 📖	mathematical	—	`Set` `instHasSubset` `add` `Ici` `PartialOrder.toPreorder` `Ioi`	—	`addRightMono_of_addRightStrictMono` `add_lt_add_of_le_of_lt`
`Ici_mul_Ici_eq` 📖	mathematical	—	`Set` `mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Ici`	—	`Subset.antisymm` `Ici_mul_Ici_subset'` `CanonicallyOrderedMul.toMulLeftMono` `mem_mul` `ExistsMulOfLE.exists_mul_of_le` `CanonicallyOrderedMul.toExistsMulOfLE` `mem_Ici` `subset_def`
`Ici_mul_Ici_subset'` 📖	mathematical	—	`Set` `instHasSubset` `mul` `Ici`	—	`mul_le_mul'`
`Ici_mul_Ioi_subset'` 📖	mathematical	—	`Set` `instHasSubset` `mul` `Ici` `PartialOrder.toPreorder` `Ioi`	—	`mulRightMono_of_mulRightStrictMono` `mul_lt_mul_of_le_of_lt`
`Ici_nsmul_eq` 📖	mathematical	—	`Set` `NSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toAdd` `Ici` `AddMonoid.toNatSMul`	—	`one_nsmul` `succ_nsmul` `one_ne_zero` `Ici_add_Ici_eq`
`Ici_one_eq_univ` 📖	mathematical	—	`Ici` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `univ`	—	`ext`
`Ici_pow_eq` 📖	mathematical	—	`Set` `NPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toMul` `Ici` `Monoid.toNatPow`	—	`pow_one` `pow_succ` `Ici_mul_Ici_eq`
`Ici_zero_eq_univ` 📖	mathematical	—	`Ici` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `univ`	—	`ext` `mem_Ici` `zero_le` `mem_univ`
`Ico_add_Icc_subset` 📖	mathematical	—	`Set` `instHasSubset` `add` `Ico` `PartialOrder.toPreorder` `Icc`	—	`addLeftMono_of_addLeftStrictMono` `addRightMono_of_addRightStrictMono` `add_le_add` `add_lt_add_of_lt_of_le`
`Ico_add_Ioc_subset` 📖	mathematical	—	`Set` `instHasSubset` `add` `Ico` `PartialOrder.toPreorder` `Ioc` `Ioo`	—	`addLeftMono_of_addLeftStrictMono` `addRightMono_of_addRightStrictMono` `add_lt_add_of_le_of_lt` `add_lt_add_of_lt_of_le`
`Ico_mul_Icc_subset'` 📖	mathematical	—	`Set` `instHasSubset` `mul` `Ico` `PartialOrder.toPreorder` `Icc`	—	`mulLeftMono_of_mulLeftStrictMono` `mulRightMono_of_mulRightStrictMono` `mul_le_mul'` `mul_lt_mul_of_lt_of_le`
`Ico_mul_Ioc_subset'` 📖	mathematical	—	`Set` `instHasSubset` `mul` `Ico` `PartialOrder.toPreorder` `Ioc` `Ioo`	—	`mulLeftMono_of_mulLeftStrictMono` `mulRightMono_of_mulRightStrictMono` `mul_lt_mul_of_le_of_lt` `mul_lt_mul_of_lt_of_le`
`Iic_add_Iic_subset` 📖	mathematical	—	`Set` `instHasSubset` `add` `Iic`	—	`add_le_add`
`Iic_add_Iio_subset` 📖	mathematical	—	`Set` `instHasSubset` `add` `Iic` `PartialOrder.toPreorder` `Iio`	—	`addRightMono_of_addRightStrictMono` `add_lt_add_of_le_of_lt`
`Iic_add_bij` 📖	mathematical	—	`BijOn` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Iic` `PartialOrder.toPreorder`	—	`InjOn.bijOn_image` `Function.Injective.injOn` `add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd` `image_add_const_Iic`
`Iic_mul_Iic_subset'` 📖	mathematical	—	`Set` `instHasSubset` `mul` `Iic`	—	`mul_le_mul'`
`Iic_mul_Iio_subset'` 📖	mathematical	—	`Set` `instHasSubset` `mul` `Iic` `PartialOrder.toPreorder` `Iio`	—	`mulRightMono_of_mulRightStrictMono` `mul_lt_mul_of_le_of_lt`
`Iic_mul_bij` 📖	mathematical	—	`BijOn` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Iic` `PartialOrder.toPreorder`	—	`InjOn.bijOn_image` `Function.Injective.injOn` `mul_left_injective` `RightCancelSemigroup.toIsRightCancelMul` `image_mul_const_Iic`
`Iio_add_Iic_subset` 📖	mathematical	—	`Set` `instHasSubset` `add` `Iio` `PartialOrder.toPreorder` `Iic`	—	`addLeftMono_of_addLeftStrictMono` `add_lt_add_of_lt_of_le`
`Iio_add_bij` 📖	mathematical	—	`BijOn` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Iio` `PartialOrder.toPreorder`	—	`InjOn.bijOn_image` `Function.Injective.injOn` `add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd` `image_add_const_Iio`
`Iio_mul_Iic_subset'` 📖	mathematical	—	`Set` `instHasSubset` `mul` `Iio` `PartialOrder.toPreorder` `Iic`	—	`mulLeftMono_of_mulLeftStrictMono` `mul_lt_mul_of_lt_of_le`
`Iio_mul_bij` 📖	mathematical	—	`BijOn` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Iio` `PartialOrder.toPreorder`	—	`InjOn.bijOn_image` `Function.Injective.injOn` `mul_left_injective` `RightCancelSemigroup.toIsRightCancelMul` `image_mul_const_Iio`
`Ioc_add_Ico_subset` 📖	mathematical	—	`Set` `instHasSubset` `add` `Ioc` `PartialOrder.toPreorder` `Ico` `Ioo`	—	`addLeftMono_of_addLeftStrictMono` `addRightMono_of_addRightStrictMono` `add_lt_add_of_lt_of_le` `add_lt_add_of_le_of_lt`
`Ioc_mul_Ico_subset'` 📖	mathematical	—	`Set` `instHasSubset` `mul` `Ioc` `PartialOrder.toPreorder` `Ico` `Ioo`	—	`mulLeftMono_of_mulLeftStrictMono` `mulRightMono_of_mulRightStrictMono` `mul_lt_mul_of_lt_of_le` `mul_lt_mul_of_le_of_lt`
`Ioi_add_Ici_subset` 📖	mathematical	—	`Set` `instHasSubset` `add` `Ioi` `PartialOrder.toPreorder` `Ici`	—	`addLeftMono_of_addLeftStrictMono` `add_lt_add_of_lt_of_le`
`Ioi_mul_Ici_subset'` 📖	mathematical	—	`Set` `instHasSubset` `mul` `Ioi` `PartialOrder.toPreorder` `Ici`	—	`mulLeftMono_of_mulLeftStrictMono` `mul_lt_mul_of_lt_of_le`
`abs_sub_le_of_uIcc_subset_uIcc` 📖	mathematical	`Set` `instHasSubset` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `abs` `AddCommGroup.toAddGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`max_sub_min_eq_abs` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `sub_le_sub` `uIcc_subset_uIcc_iff_le`
`abs_sub_left_of_mem_uIcc` 📖	mathematical	`Set` `instMembership` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `abs` `AddCommGroup.toAddGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`abs_sub_le_of_uIcc_subset_uIcc` `uIcc_subset_uIcc_left`
`abs_sub_right_of_mem_uIcc` 📖	mathematical	`Set` `instMembership` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `abs` `AddCommGroup.toAddGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`abs_sub_le_of_uIcc_subset_uIcc` `uIcc_subset_uIcc_right`
`image_add_const_Iic` 📖	mathematical	—	`image` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Iic` `PartialOrder.toPreorder`	—	`image_add_right` `preimage_add_const_Iic` `sub_neg_eq_add`
`image_add_const_Iio` 📖	mathematical	—	`image` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Iio` `PartialOrder.toPreorder`	—	`image_add_right` `preimage_add_const_Iio` `sub_neg_eq_add`
`image_add_const_uIcc` 📖	mathematical	—	`image` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`image_add_right` `preimage_add_const_uIcc` `sub_neg_eq_add`
`image_affine_Icc'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring`	`image` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `Icc`	—	`image_mul_left_Icc'` `image_add_const_Icc` `image_image`
`image_affine_Ico` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring`	`image` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `Ico`	—	`image_mul_left_Ico` `image_add_const_Ico` `image_image`
`image_affine_Ioc` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring`	`image` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `Ioc`	—	`image_mul_left_Ioc` `image_add_const_Ioc` `image_image`
`image_affine_Ioo` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring`	`image` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `Ioo`	—	`image_mul_left_Ioo` `image_add_const_Ioo` `image_image`
`image_const_add_Iic` 📖	mathematical	—	`image` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Iic` `PartialOrder.toPreorder`	—	`image_add_left` `add_comm` `preimage_add_const_Iic` `sub_neg_eq_add`
`image_const_add_Iio` 📖	mathematical	—	`image` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Iio` `PartialOrder.toPreorder`	—	`image_add_left` `add_comm` `preimage_add_const_Iio` `sub_neg_eq_add`
`image_const_add_uIcc` 📖	mathematical	—	`image` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`image_add_left` `add_comm` `preimage_add_const_uIcc` `sub_neg_eq_add`
`image_const_div_Icc` 📖	mathematical	—	`image` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Icc` `PartialOrder.toPreorder`	—	`image_comp` `image_congr` `div_eq_mul_inv` `image_inv_eq_inv` `inv_Icc` `image_mul_left` `mul_comm` `preimage_mul_const_Icc` `inv_inv`
`image_const_div_Ici` 📖	mathematical	—	`image` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ici` `PartialOrder.toPreorder` `Iic`	—	`image_comp` `image_congr` `div_eq_mul_inv` `image_inv_eq_inv` `inv_Ici` `image_mul_left` `mul_comm` `preimage_mul_const_Iic` `inv_inv`
`image_const_div_Ico` 📖	mathematical	—	`image` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ico` `PartialOrder.toPreorder` `Ioc`	—	`image_comp` `image_congr` `div_eq_mul_inv` `image_inv_eq_inv` `inv_Ico` `image_mul_left` `mul_comm` `preimage_mul_const_Ioc` `inv_inv`
`image_const_div_Iic` 📖	mathematical	—	`image` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Iic` `PartialOrder.toPreorder` `Ici`	—	`image_comp` `image_congr` `div_eq_mul_inv` `image_inv_eq_inv` `inv_Iic` `image_mul_left` `mul_comm` `preimage_mul_const_Ici` `inv_inv`
`image_const_div_Iio` 📖	mathematical	—	`image` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Iio` `PartialOrder.toPreorder` `Ioi`	—	`image_comp` `image_congr` `div_eq_mul_inv` `image_inv_eq_inv` `inv_Iio` `image_mul_left` `mul_comm` `preimage_mul_const_Ioi` `inv_inv`
`image_const_div_Ioc` 📖	mathematical	—	`image` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ioc` `PartialOrder.toPreorder` `Ico`	—	`image_comp` `image_congr` `div_eq_mul_inv` `image_inv_eq_inv` `inv_Ioc` `image_mul_left` `mul_comm` `preimage_mul_const_Ico` `inv_inv`
`image_const_div_Ioi` 📖	mathematical	—	`image` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ioi` `PartialOrder.toPreorder` `Iio`	—	`image_comp` `image_congr` `div_eq_mul_inv` `image_inv_eq_inv` `inv_Ioi` `image_mul_left` `mul_comm` `preimage_mul_const_Iio` `inv_inv`
`image_const_div_Ioo` 📖	mathematical	—	`image` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ioo` `PartialOrder.toPreorder`	—	`image_comp` `image_congr` `div_eq_mul_inv` `image_inv_eq_inv` `inv_Ioo` `image_mul_left` `mul_comm` `preimage_mul_const_Ioo` `inv_inv`
`image_const_mul_Iic` 📖	mathematical	—	`image` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Iic` `PartialOrder.toPreorder`	—	`image_mul_left` `mul_comm` `preimage_mul_const_Iic` `div_inv_eq_mul`
`image_const_mul_Iio` 📖	mathematical	—	`image` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Iio` `PartialOrder.toPreorder`	—	`image_mul_left` `mul_comm` `preimage_mul_const_Iio` `div_inv_eq_mul`
`image_const_mul_Ioi_zero` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`image` `MulZeroClass.toMul` `Ioi`	—	`image_mul_left_Ioi` `MulZeroClass.mul_zero`
`image_const_mul_uIcc` 📖	mathematical	—	`image` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`image_congr` `mul_comm` `image_mul_const_uIcc`
`image_const_sub_Icc` 📖	mathematical	—	`image` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Icc` `PartialOrder.toPreorder`	—	`image_comp` `image_congr` `sub_eq_add_neg` `image_neg_eq_neg` `neg_Icc` `image_add_left` `add_comm` `preimage_add_const_Icc` `neg_neg`
`image_const_sub_Ici` 📖	mathematical	—	`image` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ici` `PartialOrder.toPreorder` `Iic`	—	`image_comp` `image_congr` `sub_eq_add_neg` `image_neg_eq_neg` `neg_Ici` `image_add_left` `add_comm` `preimage_add_const_Iic` `neg_neg`
`image_const_sub_Ico` 📖	mathematical	—	`image` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ico` `PartialOrder.toPreorder` `Ioc`	—	`image_comp` `image_congr` `sub_eq_add_neg` `image_neg_eq_neg` `neg_Ico` `image_add_left` `add_comm` `preimage_add_const_Ioc` `neg_neg`
`image_const_sub_Iic` 📖	mathematical	—	`image` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Iic` `PartialOrder.toPreorder` `Ici`	—	`image_comp` `image_congr` `sub_eq_add_neg` `image_neg_eq_neg` `neg_Iic` `image_add_left` `add_comm` `preimage_add_const_Ici` `neg_neg`
`image_const_sub_Iio` 📖	mathematical	—	`image` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Iio` `PartialOrder.toPreorder` `Ioi`	—	`image_comp` `image_congr` `sub_eq_add_neg` `image_neg_eq_neg` `neg_Iio` `image_add_left` `add_comm` `preimage_add_const_Ioi` `neg_neg`
`image_const_sub_Ioc` 📖	mathematical	—	`image` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ioc` `PartialOrder.toPreorder` `Ico`	—	`image_comp` `image_congr` `sub_eq_add_neg` `image_neg_eq_neg` `neg_Ioc` `image_add_left` `add_comm` `preimage_add_const_Ico` `neg_neg`
`image_const_sub_Ioi` 📖	mathematical	—	`image` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ioi` `PartialOrder.toPreorder` `Iio`	—	`image_comp` `image_congr` `sub_eq_add_neg` `image_neg_eq_neg` `neg_Ioi` `image_add_left` `add_comm` `preimage_add_const_Iio` `neg_neg`
`image_const_sub_Ioo` 📖	mathematical	—	`image` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ioo` `PartialOrder.toPreorder`	—	`image_comp` `image_congr` `sub_eq_add_neg` `image_neg_eq_neg` `neg_Ioo` `image_add_left` `add_comm` `preimage_add_const_Ioo` `neg_neg`
`image_const_sub_uIcc` 📖	mathematical	—	`image` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`image_comp` `image_congr` `sub_eq_add_neg` `image_neg_eq_neg` `neg_uIcc` `image_add_left` `add_comm` `preimage_add_const_uIcc` `neg_neg`
`image_div_const_Icc` 📖	mathematical	—	`image` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Icc` `PartialOrder.toPreorder`	—	`image_congr` `div_eq_mul_inv` `image_mul_right` `inv_inv` `preimage_mul_const_Icc`
`image_div_const_Ici` 📖	mathematical	—	`image` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ici` `PartialOrder.toPreorder`	—	`image_congr` `div_eq_mul_inv` `image_mul_right` `inv_inv` `preimage_mul_const_Ici`
`image_div_const_Ico` 📖	mathematical	—	`image` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ico` `PartialOrder.toPreorder`	—	`image_congr` `div_eq_mul_inv` `image_mul_right` `inv_inv` `preimage_mul_const_Ico`
`image_div_const_Iic` 📖	mathematical	—	`image` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Iic` `PartialOrder.toPreorder`	—	`image_congr` `div_eq_mul_inv` `image_mul_right` `inv_inv` `preimage_mul_const_Iic`
`image_div_const_Iio` 📖	mathematical	—	`image` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Iio` `PartialOrder.toPreorder`	—	`image_congr` `div_eq_mul_inv` `image_mul_right` `inv_inv` `preimage_mul_const_Iio`
`image_div_const_Ioc` 📖	mathematical	—	`image` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ioc` `PartialOrder.toPreorder`	—	`image_congr` `div_eq_mul_inv` `image_mul_right` `inv_inv` `preimage_mul_const_Ioc`
`image_div_const_Ioi` 📖	mathematical	—	`image` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ioi` `PartialOrder.toPreorder`	—	`image_congr` `div_eq_mul_inv` `image_mul_right` `inv_inv` `preimage_mul_const_Ioi`
`image_div_const_Ioo` 📖	mathematical	—	`image` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ioo` `PartialOrder.toPreorder`	—	`image_congr` `div_eq_mul_inv` `image_mul_right` `inv_inv` `preimage_mul_const_Ioo`
`image_div_const_uIcc` 📖	mathematical	—	`image` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`image_congr` `div_eq_mul_inv` `image_mul_const_uIcc`
`image_inv_Icc` 📖	mathematical	—	`image` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Icc` `PartialOrder.toPreorder`	—	`image_inv_eq_inv` `inv_Icc`
`image_inv_Ici` 📖	mathematical	—	`image` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Ici` `PartialOrder.toPreorder` `Iic`	—	`image_inv_eq_inv` `inv_Ici`
`image_inv_Ico` 📖	mathematical	—	`image` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Ico` `PartialOrder.toPreorder` `Ioc`	—	`image_inv_eq_inv` `inv_Ico`
`image_inv_Iic` 📖	mathematical	—	`image` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Iic` `PartialOrder.toPreorder` `Ici`	—	`image_inv_eq_inv` `inv_Iic`
`image_inv_Iio` 📖	mathematical	—	`image` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Iio` `PartialOrder.toPreorder` `Ioi`	—	`image_inv_eq_inv` `inv_Iio`
`image_inv_Ioc` 📖	mathematical	—	`image` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Ioc` `PartialOrder.toPreorder` `Ico`	—	`image_inv_eq_inv` `inv_Ioc`
`image_inv_Ioi` 📖	mathematical	—	`image` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Ioi` `PartialOrder.toPreorder` `Iio`	—	`image_inv_eq_inv` `inv_Ioi`
`image_inv_Ioo` 📖	mathematical	—	`image` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Ioo` `PartialOrder.toPreorder`	—	`image_inv_eq_inv` `inv_Ioo`
`image_mul_const_Iic` 📖	mathematical	—	`image` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Iic` `PartialOrder.toPreorder`	—	`image_mul_right` `preimage_mul_const_Iic` `div_inv_eq_mul`
`image_mul_const_Iio` 📖	mathematical	—	`image` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Iio` `PartialOrder.toPreorder`	—	`image_mul_right` `preimage_mul_const_Iio` `div_inv_eq_mul`
`image_mul_const_uIcc` 📖	mathematical	—	`image` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`image_congr` `MulZeroClass.mul_zero` `Nonempty.image_const` `uIcc_of_le` `Icc_self` `Equiv.image_eq_preimage_symm` `div_eq_mul_inv` `preimage_div_const_uIcc`
`image_mul_left_Icc` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`image` `MulZeroClass.toMul` `Icc`	—	`LE.le.eq_or_lt` `image_congr` `MulZeroClass.zero_mul` `Nonempty.image_const` `nonempty_Icc` `Icc_self` `image_mul_left_Icc'`
`image_mul_left_Icc'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`image` `MulZeroClass.toMul` `Icc`	—	`OrderIso.image_Icc`
`image_mul_left_Ici` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`image` `MulZeroClass.toMul` `Ici`	—	`OrderIso.image_Ici`
`image_mul_left_Ico` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`image` `MulZeroClass.toMul` `Ico`	—	`OrderIso.image_Ico`
`image_mul_left_Iic` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`image` `MulZeroClass.toMul` `Iic`	—	`OrderIso.image_Iic`
`image_mul_left_Iio` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`image` `MulZeroClass.toMul` `Iio`	—	`OrderIso.image_Iio`
`image_mul_left_Ioc` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`image` `MulZeroClass.toMul` `Ioc`	—	`OrderIso.image_Ioc`
`image_mul_left_Ioi` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`image` `MulZeroClass.toMul` `Ioi`	—	`OrderIso.image_Ioi`
`image_mul_left_Ioo` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`image` `MulZeroClass.toMul` `Ioo`	—	`OrderIso.image_Ioo`
`image_mul_right_Icc` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`image` `MulZeroClass.toMul` `Icc`	—	`eq_or_lt_of_le` `image_congr` `MulZeroClass.mul_zero` `Nonempty.image_const` `nonempty_Icc` `Icc_self` `image_mul_right_Icc'`
`image_mul_right_Icc'` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`image` `MulZeroClass.toMul` `Icc`	—	`OrderIso.image_Icc`
`image_mul_right_Ico` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`image` `MulZeroClass.toMul` `Ico`	—	`OrderIso.image_Ico`
`image_mul_right_Ioc` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`image` `MulZeroClass.toMul` `Ioc`	—	`OrderIso.image_Ioc`
`image_mul_right_Ioo` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`image` `MulZeroClass.toMul` `Ioo`	—	`OrderIso.image_Ioo`
`image_neg_Icc` 📖	mathematical	—	`image` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Icc` `PartialOrder.toPreorder`	—	`image_neg_eq_neg` `neg_Icc`
`image_neg_Ici` 📖	mathematical	—	`image` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ici` `PartialOrder.toPreorder` `Iic`	—	`image_neg_eq_neg` `neg_Ici`
`image_neg_Ico` 📖	mathematical	—	`image` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ico` `PartialOrder.toPreorder` `Ioc`	—	`image_neg_eq_neg` `neg_Ico`
`image_neg_Iic` 📖	mathematical	—	`image` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Iic` `PartialOrder.toPreorder` `Ici`	—	`image_neg_eq_neg` `neg_Iic`
`image_neg_Iio` 📖	mathematical	—	`image` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Iio` `PartialOrder.toPreorder` `Ioi`	—	`image_neg_eq_neg` `neg_Iio`
`image_neg_Ioc` 📖	mathematical	—	`image` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ioc` `PartialOrder.toPreorder` `Ico`	—	`image_neg_eq_neg` `neg_Ioc`
`image_neg_Ioi` 📖	mathematical	—	`image` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ioi` `PartialOrder.toPreorder` `Iio`	—	`image_neg_eq_neg` `neg_Ioi`
`image_neg_Ioo` 📖	mathematical	—	`image` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ioo` `PartialOrder.toPreorder`	—	`image_neg_eq_neg` `neg_Ioo`
`image_neg_uIcc` 📖	mathematical	—	`image` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`image_neg_eq_neg` `neg_uIcc`
`image_sub_const_Icc` 📖	mathematical	—	`image` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Icc` `PartialOrder.toPreorder`	—	`image_congr` `sub_eq_add_neg` `image_add_right` `neg_neg` `preimage_add_const_Icc`
`image_sub_const_Ici` 📖	mathematical	—	`image` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ici` `PartialOrder.toPreorder`	—	`image_congr` `sub_eq_add_neg` `image_add_right` `neg_neg` `preimage_add_const_Ici`
`image_sub_const_Ico` 📖	mathematical	—	`image` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ico` `PartialOrder.toPreorder`	—	`image_congr` `sub_eq_add_neg` `image_add_right` `neg_neg` `preimage_add_const_Ico`
`image_sub_const_Iic` 📖	mathematical	—	`image` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Iic` `PartialOrder.toPreorder`	—	`image_congr` `sub_eq_add_neg` `image_add_right` `neg_neg` `preimage_add_const_Iic`
`image_sub_const_Iio` 📖	mathematical	—	`image` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Iio` `PartialOrder.toPreorder`	—	`image_congr` `sub_eq_add_neg` `image_add_right` `neg_neg` `preimage_add_const_Iio`
`image_sub_const_Ioc` 📖	mathematical	—	`image` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ioc` `PartialOrder.toPreorder`	—	`image_congr` `sub_eq_add_neg` `image_add_right` `neg_neg` `preimage_add_const_Ioc`
`image_sub_const_Ioi` 📖	mathematical	—	`image` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ioi` `PartialOrder.toPreorder`	—	`image_congr` `sub_eq_add_neg` `image_add_right` `neg_neg` `preimage_add_const_Ioi`
`image_sub_const_Ioo` 📖	mathematical	—	`image` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ioo` `PartialOrder.toPreorder`	—	`image_congr` `sub_eq_add_neg` `image_add_right` `neg_neg` `preimage_add_const_Ioo`
`image_sub_const_uIcc` 📖	mathematical	—	`image` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`image_congr` `sub_eq_add_neg` `image_add_right` `neg_neg` `add_comm` `preimage_const_add_uIcc`
`inv_Icc` 📖	mathematical	—	`Set` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Icc` `PartialOrder.toPreorder`	—	`inter_inv` `inv_Ici` `inv_Iic` `inter_comm`
`inv_Ici` 📖	mathematical	—	`Set` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Ici` `PartialOrder.toPreorder` `Iic`	—	`ext` `le_inv'` `IsOrderedMonoid.toMulLeftMono` `covariant_swap_mul_of_covariant_mul`
`inv_Ico` 📖	mathematical	—	`Set` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Ico` `PartialOrder.toPreorder` `Ioc`	—	`inter_inv` `inv_Ici` `inv_Iio` `inter_comm`
`inv_Iic` 📖	mathematical	—	`Set` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Iic` `PartialOrder.toPreorder` `Ici`	—	`ext` `inv_le'` `IsOrderedMonoid.toMulLeftMono` `covariant_swap_mul_of_covariant_mul`
`inv_Iio` 📖	mathematical	—	`Set` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Iio` `PartialOrder.toPreorder` `Ioi`	—	`ext` `inv_lt'` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `LeftCancelSemigroup.toIsLeftCancelMul` `IsOrderedMonoid.toMulLeftMono` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `RightCancelSemigroup.toIsRightCancelMul` `covariant_swap_mul_of_covariant_mul`
`inv_Iio₀` 📖	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`	`Set` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Iio` `Ioo`	—	`inv_eq_iff_eq_inv` `inv_Ioo_0_right` `inv_neg''` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `inv_inv`
`inv_Ioc` 📖	mathematical	—	`Set` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Ioc` `PartialOrder.toPreorder` `Ico`	—	`inter_comm` `inter_inv` `inv_Iic` `inv_Ioi`
`inv_Ioi` 📖	mathematical	—	`Set` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Ioi` `PartialOrder.toPreorder` `Iio`	—	`ext` `lt_inv'` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `LeftCancelSemigroup.toIsLeftCancelMul` `IsOrderedMonoid.toMulLeftMono` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `RightCancelSemigroup.toIsRightCancelMul` `covariant_swap_mul_of_covariant_mul`
`inv_Ioi₀` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`Set` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `Ioi` `Ioo`	—	`inv_eq_iff_eq_inv` `inv_Ioo_0_left` `inv_pos` `inv_inv`
`inv_Ioo` 📖	mathematical	—	`Set` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Ioo` `PartialOrder.toPreorder`	—	`inter_comm` `inter_inv` `inv_Iio` `inv_Ioi`
`inv_Ioo_0_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`Set` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `Ioo` `Ioi`	—	`ext` `inv_lt_of_inv_lt₀` `inv_pos` `LT.lt.trans`
`inv_Ioo_0_right` 📖	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`	`Set` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Ioo` `Iio`	—	`ext` `lt_inv_of_neg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `inv_neg''` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `LT.lt.trans`
`inv_uIcc` 📖	mathematical	—	`Set` `inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`inv_Icc` `inv_sup` `IsOrderedMonoid.toMulLeftMono` `covariant_swap_mul_of_covariant_mul` `inv_inf`
`neg_Icc` 📖	mathematical	—	`Set` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Icc` `PartialOrder.toPreorder`	—	`inter_neg` `neg_Ici` `neg_Iic` `inter_comm`
`neg_Ici` 📖	mathematical	—	`Set` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ici` `PartialOrder.toPreorder` `Iic`	—	`ext` `le_neg` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add`
`neg_Ico` 📖	mathematical	—	`Set` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ico` `PartialOrder.toPreorder` `Ioc`	—	`inter_neg` `neg_Ici` `neg_Iio` `inter_comm`
`neg_Iic` 📖	mathematical	—	`Set` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Iic` `PartialOrder.toPreorder` `Ici`	—	`ext` `neg_le` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add`
`neg_Iio` 📖	mathematical	—	`Set` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Iio` `PartialOrder.toPreorder` `Ioi`	—	`ext` `neg_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add`
`neg_Ioc` 📖	mathematical	—	`Set` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ioc` `PartialOrder.toPreorder` `Ico`	—	`inter_comm` `inter_neg` `neg_Iic` `neg_Ioi`
`neg_Ioi` 📖	mathematical	—	`Set` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ioi` `PartialOrder.toPreorder` `Iio`	—	`ext` `lt_neg` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add`
`neg_Ioo` 📖	mathematical	—	`Set` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ioo` `PartialOrder.toPreorder`	—	`inter_comm` `inter_neg` `neg_Iio` `neg_Ioi`
`neg_uIcc` 📖	mathematical	—	`Set` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`neg_Icc` `neg_sup` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `neg_inf`
`preimage_add_const_Icc` 📖	mathematical	—	`preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Icc` `PartialOrder.toPreorder` `SubNegMonoid.toSub`	—	`preimage_add_const_Ici` `preimage_add_const_Iic`
`preimage_add_const_Ici` 📖	mathematical	—	`preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ici` `PartialOrder.toPreorder` `SubNegMonoid.toSub`	—	`ext` `sub_le_iff_le_add` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono`
`preimage_add_const_Ico` 📖	mathematical	—	`preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ico` `PartialOrder.toPreorder` `SubNegMonoid.toSub`	—	`preimage_add_const_Ici` `preimage_add_const_Iio`
`preimage_add_const_Iic` 📖	mathematical	—	`preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Iic` `PartialOrder.toPreorder` `SubNegMonoid.toSub`	—	`ext` `le_sub_iff_add_le` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono`
`preimage_add_const_Iio` 📖	mathematical	—	`preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Iio` `PartialOrder.toPreorder` `SubNegMonoid.toSub`	—	`ext` `lt_sub_iff_add_lt` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono`
`preimage_add_const_Ioc` 📖	mathematical	—	`preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ioc` `PartialOrder.toPreorder` `SubNegMonoid.toSub`	—	`preimage_add_const_Ioi` `preimage_add_const_Iic`
`preimage_add_const_Ioi` 📖	mathematical	—	`preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ioi` `PartialOrder.toPreorder` `SubNegMonoid.toSub`	—	`ext` `sub_lt_iff_lt_add` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono`
`preimage_add_const_Ioo` 📖	mathematical	—	`preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ioo` `PartialOrder.toPreorder` `SubNegMonoid.toSub`	—	`preimage_add_const_Ioi` `preimage_add_const_Iio`
`preimage_add_const_uIcc` 📖	mathematical	—	`preimage` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`add_comm` `preimage_const_add_uIcc`
`preimage_const_add_Icc` 📖	mathematical	—	`preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Icc` `PartialOrder.toPreorder` `SubNegMonoid.toSub`	—	`preimage_const_add_Ici` `preimage_const_add_Iic`
`preimage_const_add_Ici` 📖	mathematical	—	`preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ici` `PartialOrder.toPreorder` `SubNegMonoid.toSub`	—	`ext` `sub_le_iff_le_add'` `IsOrderedAddMonoid.toAddLeftMono`
`preimage_const_add_Ico` 📖	mathematical	—	`preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ico` `PartialOrder.toPreorder` `SubNegMonoid.toSub`	—	`preimage_const_add_Ici` `preimage_const_add_Iio`
`preimage_const_add_Iic` 📖	mathematical	—	`preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Iic` `PartialOrder.toPreorder` `SubNegMonoid.toSub`	—	`ext` `le_sub_iff_add_le'` `IsOrderedAddMonoid.toAddLeftMono`
`preimage_const_add_Iio` 📖	mathematical	—	`preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Iio` `PartialOrder.toPreorder` `SubNegMonoid.toSub`	—	`ext` `lt_sub_iff_add_lt'` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono`
`preimage_const_add_Ioc` 📖	mathematical	—	`preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ioc` `PartialOrder.toPreorder` `SubNegMonoid.toSub`	—	`preimage_const_add_Ioi` `preimage_const_add_Iic`
`preimage_const_add_Ioi` 📖	mathematical	—	`preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ioi` `PartialOrder.toPreorder` `SubNegMonoid.toSub`	—	`ext` `sub_lt_iff_lt_add'` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono`
`preimage_const_add_Ioo` 📖	mathematical	—	`preimage` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ioo` `PartialOrder.toPreorder` `SubNegMonoid.toSub`	—	`preimage_const_add_Ioi` `preimage_const_add_Iio`
`preimage_const_add_uIcc` 📖	mathematical	—	`preimage` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`preimage_const_add_Icc` `min_sub_sub_right` `max_sub_sub_right`
`preimage_const_div_Icc` 📖	mathematical	—	`preimage` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Icc` `PartialOrder.toPreorder`	—	`preimage_const_div_Ici` `preimage_const_div_Iic` `inter_comm`
`preimage_const_div_Ici` 📖	mathematical	—	`preimage` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ici` `PartialOrder.toPreorder` `Iic`	—	`ext` `le_div_comm` `IsOrderedMonoid.toMulLeftMono`
`preimage_const_div_Ico` 📖	mathematical	—	`preimage` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ico` `PartialOrder.toPreorder` `Ioc`	—	`preimage_const_div_Ici` `preimage_const_div_Iio` `inter_comm`
`preimage_const_div_Iic` 📖	mathematical	—	`preimage` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Iic` `PartialOrder.toPreorder` `Ici`	—	`ext` `div_le_comm` `IsOrderedMonoid.toMulLeftMono`
`preimage_const_div_Iio` 📖	mathematical	—	`preimage` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Iio` `PartialOrder.toPreorder` `Ioi`	—	`ext` `div_lt_comm` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `LeftCancelSemigroup.toIsLeftCancelMul` `IsOrderedMonoid.toMulLeftMono`
`preimage_const_div_Ioc` 📖	mathematical	—	`preimage` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ioc` `PartialOrder.toPreorder` `Ico`	—	`inter_comm` `preimage_const_div_Iic` `preimage_const_div_Ioi`
`preimage_const_div_Ioi` 📖	mathematical	—	`preimage` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ioi` `PartialOrder.toPreorder` `Iio`	—	`ext` `lt_div_comm` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `LeftCancelSemigroup.toIsLeftCancelMul` `IsOrderedMonoid.toMulLeftMono`
`preimage_const_div_Ioo` 📖	mathematical	—	`preimage` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ioo` `PartialOrder.toPreorder`	—	`inter_comm` `preimage_const_div_Iio` `preimage_const_div_Ioi`
`preimage_const_mul_Icc` 📖	mathematical	—	`preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Icc` `PartialOrder.toPreorder` `DivInvMonoid.toDiv`	—	`preimage_const_mul_Ici` `preimage_const_mul_Iic`
`preimage_const_mul_Icc_of_neg` 📖	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`	`preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Icc` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`mul_comm` `preimage_mul_const_Icc_of_neg`
`preimage_const_mul_Icc₀` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero`	`preimage` `MulZeroClass.toMul` `Icc` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`preimage_const_mul_Ici₀` `preimage_const_mul_Iic₀`
`preimage_const_mul_Ici` 📖	mathematical	—	`preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ici` `PartialOrder.toPreorder` `DivInvMonoid.toDiv`	—	`ext` `div_le_iff_le_mul'` `IsOrderedMonoid.toMulLeftMono`
`preimage_const_mul_Ici_of_neg` 📖	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`	`preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Ici` `Iic` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`mul_comm` `preimage_mul_const_Ici_of_neg`
`preimage_const_mul_Ici₀` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero`	`preimage` `MulZeroClass.toMul` `Ici` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`ext` `div_le_iff₀'`
`preimage_const_mul_Ico` 📖	mathematical	—	`preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ico` `PartialOrder.toPreorder` `DivInvMonoid.toDiv`	—	`preimage_const_mul_Ici` `preimage_const_mul_Iio`
`preimage_const_mul_Ico_of_neg` 📖	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`	`preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Ico` `Ioc` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`mul_comm` `preimage_mul_const_Ico_of_neg`
`preimage_const_mul_Ico₀` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero`	`preimage` `MulZeroClass.toMul` `Ico` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`preimage_const_mul_Ici₀` `preimage_const_mul_Iio₀`
`preimage_const_mul_Iic` 📖	mathematical	—	`preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Iic` `PartialOrder.toPreorder` `DivInvMonoid.toDiv`	—	`ext` `le_div_iff_mul_le'` `IsOrderedMonoid.toMulLeftMono`
`preimage_const_mul_Iic_of_neg` 📖	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`	`preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Iic` `Ici` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`mul_comm` `preimage_mul_const_Iic_of_neg`
`preimage_const_mul_Iic₀` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero`	`preimage` `MulZeroClass.toMul` `Iic` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`ext` `le_div_iff₀'`
`preimage_const_mul_Iio` 📖	mathematical	—	`preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Iio` `PartialOrder.toPreorder` `DivInvMonoid.toDiv`	—	`ext` `lt_div_iff_mul_lt'` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `LeftCancelSemigroup.toIsLeftCancelMul` `IsOrderedMonoid.toMulLeftMono`
`preimage_const_mul_Iio_of_neg` 📖	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`	`preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Iio` `Ioi` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`mul_comm` `preimage_mul_const_Iio_of_neg`
`preimage_const_mul_Iio₀` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero`	`preimage` `MulZeroClass.toMul` `Iio` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`ext` `lt_div_iff₀'`
`preimage_const_mul_Ioc` 📖	mathematical	—	`preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ioc` `PartialOrder.toPreorder` `DivInvMonoid.toDiv`	—	`preimage_const_mul_Ioi` `preimage_const_mul_Iic`
`preimage_const_mul_Ioc_of_neg` 📖	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`	`preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Ioc` `Ico` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`mul_comm` `preimage_mul_const_Ioc_of_neg`
`preimage_const_mul_Ioc₀` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero`	`preimage` `MulZeroClass.toMul` `Ioc` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`preimage_const_mul_Ioi₀` `preimage_const_mul_Iic₀`
`preimage_const_mul_Ioi` 📖	mathematical	—	`preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ioi` `PartialOrder.toPreorder` `DivInvMonoid.toDiv`	—	`ext` `div_lt_iff_lt_mul'` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `LeftCancelSemigroup.toIsLeftCancelMul` `IsOrderedMonoid.toMulLeftMono`
`preimage_const_mul_Ioi_of_neg` 📖	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`	`preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Ioi` `Iio` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`mul_comm` `preimage_mul_const_Ioi_of_neg`
`preimage_const_mul_Ioi_or_Iio` 📖	—	`Set` `instMembership` `setOf` `Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Iio` `preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	—	`lt_or_gt_of_ne` `preimage_const_mul_Ioi_of_neg` `div_eq_inv_mul` `preimage_const_mul_Ioi₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `preimage_const_mul_Iio_of_neg` `preimage_const_mul_Iio₀`
`preimage_const_mul_Ioi₀` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero`	`preimage` `MulZeroClass.toMul` `Ioi` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`ext` `div_lt_iff₀'`
`preimage_const_mul_Ioo` 📖	mathematical	—	`preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ioo` `PartialOrder.toPreorder` `DivInvMonoid.toDiv`	—	`preimage_const_mul_Ioi` `preimage_const_mul_Iio`
`preimage_const_mul_Ioo_of_neg` 📖	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`	`preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Ioo` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`mul_comm` `preimage_mul_const_Ioo_of_neg`
`preimage_const_mul_Ioo₀` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero`	`preimage` `MulZeroClass.toMul` `Ioo` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`preimage_const_mul_Ioi₀` `preimage_const_mul_Iio₀`
`preimage_const_mul_uIcc` 📖	mathematical	—	`preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`preimage_mul_const_uIcc` `mul_comm`
`preimage_const_sub_Icc` 📖	mathematical	—	`preimage` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Icc` `PartialOrder.toPreorder`	—	`preimage_const_sub_Ici` `preimage_const_sub_Iic` `inter_comm`
`preimage_const_sub_Ici` 📖	mathematical	—	`preimage` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ici` `PartialOrder.toPreorder` `Iic`	—	`ext` `le_sub_comm` `IsOrderedAddMonoid.toAddLeftMono`
`preimage_const_sub_Ico` 📖	mathematical	—	`preimage` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ico` `PartialOrder.toPreorder` `Ioc`	—	`preimage_const_sub_Ici` `preimage_const_sub_Iio` `inter_comm`
`preimage_const_sub_Iic` 📖	mathematical	—	`preimage` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Iic` `PartialOrder.toPreorder` `Ici`	—	`ext` `sub_le_comm` `IsOrderedAddMonoid.toAddLeftMono`
`preimage_const_sub_Iio` 📖	mathematical	—	`preimage` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Iio` `PartialOrder.toPreorder` `Ioi`	—	`ext` `sub_lt_comm` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono`
`preimage_const_sub_Ioc` 📖	mathematical	—	`preimage` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ioc` `PartialOrder.toPreorder` `Ico`	—	`inter_comm` `preimage_const_sub_Iic` `preimage_const_sub_Ioi`
`preimage_const_sub_Ioi` 📖	mathematical	—	`preimage` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ioi` `PartialOrder.toPreorder` `Iio`	—	`ext` `lt_sub_comm` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono`
`preimage_const_sub_Ioo` 📖	mathematical	—	`preimage` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ioo` `PartialOrder.toPreorder`	—	`inter_comm` `preimage_const_sub_Iio` `preimage_const_sub_Ioi`
`preimage_const_sub_uIcc` 📖	mathematical	—	`preimage` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`preimage_const_sub_Icc` `sub_eq_add_neg` `min_add_add_left` `IsOrderedAddMonoid.toAddLeftMono` `min_neg_neg` `max_add_add_left` `max_neg_neg`
`preimage_div_const_Icc` 📖	mathematical	—	`preimage` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Icc` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	—	`div_eq_mul_inv` `preimage_mul_const_Icc` `inv_inv`
`preimage_div_const_Ici` 📖	mathematical	—	`preimage` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ici` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	—	`div_eq_mul_inv` `preimage_mul_const_Ici` `inv_inv`
`preimage_div_const_Ico` 📖	mathematical	—	`preimage` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ico` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	—	`div_eq_mul_inv` `preimage_mul_const_Ico` `inv_inv`
`preimage_div_const_Iic` 📖	mathematical	—	`preimage` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Iic` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	—	`div_eq_mul_inv` `preimage_mul_const_Iic` `inv_inv`
`preimage_div_const_Iio` 📖	mathematical	—	`preimage` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Iio` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	—	`div_eq_mul_inv` `preimage_mul_const_Iio` `inv_inv`
`preimage_div_const_Ioc` 📖	mathematical	—	`preimage` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ioc` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	—	`div_eq_mul_inv` `preimage_mul_const_Ioc` `inv_inv`
`preimage_div_const_Ioi` 📖	mathematical	—	`preimage` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ioi` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	—	`div_eq_mul_inv` `preimage_mul_const_Ioi` `inv_inv`
`preimage_div_const_Ioo` 📖	mathematical	—	`preimage` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ioo` `PartialOrder.toPreorder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid`	—	`div_eq_mul_inv` `preimage_mul_const_Ioo` `inv_inv`
`preimage_div_const_uIcc` 📖	mathematical	—	`preimage` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`div_eq_mul_inv` `preimage_mul_const_uIcc` `inv_ne_zero` `inv_inv`
`preimage_mul_const_Icc` 📖	mathematical	—	`preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Icc` `PartialOrder.toPreorder` `DivInvMonoid.toDiv`	—	`preimage_mul_const_Ici` `preimage_mul_const_Iic`
`preimage_mul_const_Icc_of_neg` 📖	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`	`preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Icc` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`preimage_mul_const_Ici_of_neg` `preimage_mul_const_Iic_of_neg` `inter_comm`
`preimage_mul_const_Icc₀` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`preimage` `MulZeroClass.toMul` `Icc` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`preimage_mul_const_Ici₀` `preimage_mul_const_Iic₀`
`preimage_mul_const_Ici` 📖	mathematical	—	`preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ici` `PartialOrder.toPreorder` `DivInvMonoid.toDiv`	—	`ext` `div_le_iff_le_mul` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono`
`preimage_mul_const_Ici_of_neg` 📖	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`	`preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Ici` `Iic` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`ext` `le_div_iff_of_neg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono`
`preimage_mul_const_Ici₀` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`preimage` `MulZeroClass.toMul` `Ici` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`division_def` `OrderIso.preimage_Ici`
`preimage_mul_const_Ico` 📖	mathematical	—	`preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ico` `PartialOrder.toPreorder` `DivInvMonoid.toDiv`	—	`preimage_mul_const_Ici` `preimage_mul_const_Iio`
`preimage_mul_const_Ico_of_neg` 📖	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`	`preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Ico` `Ioc` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`preimage_mul_const_Ici_of_neg` `preimage_mul_const_Iio_of_neg` `inter_comm`
`preimage_mul_const_Ico₀` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`preimage` `MulZeroClass.toMul` `Ico` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`preimage_mul_const_Ici₀` `preimage_mul_const_Iio₀`
`preimage_mul_const_Iic` 📖	mathematical	—	`preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Iic` `PartialOrder.toPreorder` `DivInvMonoid.toDiv`	—	`ext` `le_div_iff_mul_le` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono`
`preimage_mul_const_Iic_of_neg` 📖	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`	`preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Iic` `Ici` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`ext` `div_le_iff_of_neg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono`
`preimage_mul_const_Iic₀` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`preimage` `MulZeroClass.toMul` `Iic` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`division_def` `OrderIso.preimage_Iic`
`preimage_mul_const_Iio` 📖	mathematical	—	`preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Iio` `PartialOrder.toPreorder` `DivInvMonoid.toDiv`	—	`ext` `lt_div_iff_mul_lt` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `RightCancelSemigroup.toIsRightCancelMul` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono`
`preimage_mul_const_Iio_of_neg` 📖	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`	`preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Iio` `Ioi` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`ext` `div_lt_iff_of_neg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono`
`preimage_mul_const_Iio₀` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`preimage` `MulZeroClass.toMul` `Iio` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`division_def` `OrderIso.preimage_Iio`
`preimage_mul_const_Ioc` 📖	mathematical	—	`preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ioc` `PartialOrder.toPreorder` `DivInvMonoid.toDiv`	—	`preimage_mul_const_Ioi` `preimage_mul_const_Iic`
`preimage_mul_const_Ioc_of_neg` 📖	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`	`preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Ioc` `Ico` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`inter_comm` `preimage_mul_const_Iic_of_neg` `preimage_mul_const_Ioi_of_neg`
`preimage_mul_const_Ioc₀` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`preimage` `MulZeroClass.toMul` `Ioc` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`preimage_mul_const_Ioi₀` `preimage_mul_const_Iic₀`
`preimage_mul_const_Ioi` 📖	mathematical	—	`preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ioi` `PartialOrder.toPreorder` `DivInvMonoid.toDiv`	—	`ext` `div_lt_iff_lt_mul` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `RightCancelSemigroup.toIsRightCancelMul` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono`
`preimage_mul_const_Ioi_of_neg` 📖	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`	`preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Ioi` `Iio` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`ext` `lt_div_iff_of_neg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono`
`preimage_mul_const_Ioi₀` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`preimage` `MulZeroClass.toMul` `Ioi` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`division_def` `OrderIso.preimage_Ioi`
`preimage_mul_const_Ioo` 📖	mathematical	—	`preimage` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Ioo` `PartialOrder.toPreorder` `DivInvMonoid.toDiv`	—	`preimage_mul_const_Ioi` `preimage_mul_const_Iio`
`preimage_mul_const_Ioo_of_neg` 📖	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`	`preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Ioo` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`inter_comm` `preimage_mul_const_Iio_of_neg` `preimage_mul_const_Ioi_of_neg`
`preimage_mul_const_Ioo₀` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`preimage` `MulZeroClass.toMul` `Ioo` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`preimage_mul_const_Ioi₀` `preimage_mul_const_Iio₀`
`preimage_mul_const_uIcc` 📖	mathematical	—	`preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing`	—	`lt_or_gt_of_ne` `preimage_mul_const_Icc_of_neg` `min_div_div_right_of_nonpos` `LT.lt.le` `max_div_div_right_of_nonpos` `preimage_mul_const_Icc₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `min_div_div_right` `max_div_div_right`
`preimage_sub_const_Icc` 📖	mathematical	—	`preimage` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Icc` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid`	—	`sub_eq_add_neg` `preimage_add_const_Icc` `neg_neg`
`preimage_sub_const_Ici` 📖	mathematical	—	`preimage` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ici` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid`	—	`sub_eq_add_neg` `preimage_add_const_Ici` `neg_neg`
`preimage_sub_const_Ico` 📖	mathematical	—	`preimage` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ico` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid`	—	`sub_eq_add_neg` `preimage_add_const_Ico` `neg_neg`
`preimage_sub_const_Iic` 📖	mathematical	—	`preimage` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Iic` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid`	—	`sub_eq_add_neg` `preimage_add_const_Iic` `neg_neg`
`preimage_sub_const_Iio` 📖	mathematical	—	`preimage` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Iio` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid`	—	`sub_eq_add_neg` `preimage_add_const_Iio` `neg_neg`
`preimage_sub_const_Ioc` 📖	mathematical	—	`preimage` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ioc` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid`	—	`sub_eq_add_neg` `preimage_add_const_Ioc` `neg_neg`
`preimage_sub_const_Ioi` 📖	mathematical	—	`preimage` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ioi` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid`	—	`sub_eq_add_neg` `preimage_add_const_Ioi` `neg_neg`
`preimage_sub_const_Ioo` 📖	mathematical	—	`preimage` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ioo` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid`	—	`sub_eq_add_neg` `preimage_add_const_Ioo` `neg_neg`
`preimage_sub_const_uIcc` 📖	mathematical	—	`preimage` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`sub_eq_add_neg` `preimage_add_const_uIcc` `neg_neg`
`smul_Icc` 📖	mathematical	—	`Set` `smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `CommMonoid.toMonoid` `MulAction.toSemigroupAction` `Monoid.toMulAction` `Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`ext` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `exists_one_le_mul_of_le` `le_mul_of_one_le_right'` `mul_le_mul_iff_left` `mul_assoc`
`vadd_Icc` 📖	mathematical	—	`HVAdd.hVAdd` `Set` `instHVAdd` `vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`ext` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `exists_nonneg_add_of_le` `le_add_of_nonneg_right` `add_le_add_iff_left` `add_assoc`

---

← Back to Index