PosPart

📁 Source: Mathlib/Algebra/Order/Group/PosPart.lean

Statistics

Metric	Count
Definitions `instLeOnePart`, `instNegPart`, `instOneLePart`, `instPosPart`	4
Theorems `leOnePart_apply`, `leOnePart_def`, `negPart_apply`, `negPart_def`, `oneLePart_apply`, `oneLePart_def`, `posPart_apply`, `posPart_def`, `abs_add_eq_two_nsmul_posPart`, `abs_sub_eq_two_nsmul_negPart`, `add_abs_eq_two_nsmul_posPart`, `div_mabs_eq_inv_leOnePart_sq`, `inf_eq_div_oneLePart_div`, `inf_eq_sub_posPart_sub`, `inv_le_leOnePart`, `leOnePart_anti`, `leOnePart_def`, `leOnePart_div_oneLePart`, `leOnePart_eq_inv`, `leOnePart_eq_inv'`, `leOnePart_eq_inv_inf_one`, `leOnePart_eq_ite`, `leOnePart_eq_ite_lt`, `leOnePart_eq_one`, `leOnePart_eq_one'`, `leOnePart_inv`, `leOnePart_le_one`, `leOnePart_le_one'`, `leOnePart_lt`, `leOnePart_max`, `leOnePart_min`, `leOnePart_mul_oneLePart`, `leOnePart_of_le_one`, `leOnePart_of_one_le`, `leOnePart_one`, `le_iff_oneLePart_leOnePart`, `le_iff_posPart_negPart`, `le_oneLePart`, `le_posPart`, `mabs_div_eq_leOnePart_sq`, `mabs_mul_eq_oneLePart_sq`, `mul_mabs_eq_oneLePart_sq`, `negPart_add_posPart`, `negPart_anti`, `negPart_def`, `negPart_eq_ite`, `negPart_eq_ite_lt`, `negPart_eq_neg`, `negPart_eq_neg'`, `negPart_eq_neg_inf_zero`, `negPart_eq_zero`, `negPart_eq_zero'`, `negPart_lt`, `negPart_max`, `negPart_min`, `negPart_neg`, `negPart_nonneg`, `negPart_nonpos`, `negPart_nonpos'`, `negPart_of_nonneg`, `negPart_of_nonpos`, `negPart_pos`, `negPart_pos_iff`, `negPart_sub_posPart`, `negPart_zero`, `neg_le_negPart`, `oneLePart_def`, `oneLePart_div_leOnePart`, `oneLePart_eq_ite`, `oneLePart_eq_ite_lt`, `oneLePart_eq_one`, `oneLePart_eq_self`, `oneLePart_inf_leOnePart_eq_one`, `oneLePart_inv`, `oneLePart_leOnePart_inj`, `oneLePart_leOnePart_injective`, `oneLePart_le_one`, `oneLePart_lt`, `oneLePart_max`, `oneLePart_min`, `oneLePart_mono`, `oneLePart_mul_leOnePart`, `oneLePart_of_le_one`, `oneLePart_of_one_le`, `oneLePart_of_one_lt_oneLePart`, `oneLePart_one`, `one_le_leOnePart`, `one_le_oneLePart`, `one_lt_leOnePart`, `one_lt_leOnePart_iff`, `one_lt_ltOnePart`, `one_lt_ltOnePart_iff`, `one_lt_oneLePart`, `one_lt_oneLePart_iff`, `posPart_add_negPart`, `posPart_def`, `posPart_eq_ite`, `posPart_eq_ite_lt`, `posPart_eq_of_posPart_pos`, `posPart_eq_self`, `posPart_eq_zero`, `posPart_inf_negPart_eq_zero`, `posPart_lt`, `posPart_max`, `posPart_min`, `posPart_mono`, `posPart_neg`, `posPart_negPart_inj`, `posPart_negPart_injective`, `posPart_nonneg`, `posPart_nonpos`, `posPart_of_nonneg`, `posPart_of_nonpos`, `posPart_pos`, `posPart_pos_iff`, `posPart_sub_negPart`, `posPart_zero`, `sub_abs_eq_neg_two_nsmul_negPart`, `sup_eq_add_posPart_sub`, `sup_eq_mul_oneLePart_div`	120
Total	124

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`leOnePart_apply` 📖	mathematical	—	`LeOnePart.leOnePart` `instLeOnePart` `instLattice` `group`	—	—
`leOnePart_def` 📖	mathematical	—	`LeOnePart.leOnePart` `instLeOnePart` `instLattice` `group`	—	—
`negPart_apply` 📖	mathematical	—	`NegPart.negPart` `instNegPart` `instLattice` `addGroup`	—	—
`negPart_def` 📖	mathematical	—	`NegPart.negPart` `instNegPart` `instLattice` `addGroup`	—	—
`oneLePart_apply` 📖	mathematical	—	`OneLePart.oneLePart` `instOneLePart` `instLattice` `group`	—	—
`oneLePart_def` 📖	mathematical	—	`OneLePart.oneLePart` `instOneLePart` `instLattice` `group`	—	—
`posPart_apply` 📖	mathematical	—	`PosPart.posPart` `instPosPart` `instLattice` `addGroup`	—	—
`posPart_def` 📖	mathematical	—	`PosPart.posPart` `instPosPart` `instLattice` `addGroup`	—	—

(root)

Definitions

Name	Category	Theorems
`instLeOnePart` 📖	CompOp	39 math math: `oneLePart_leOnePart_injective`, `leOnePart_eq_inv_inf_one`, `leOnePart_le_one`, `leOnePart_of_one_le`, `leOnePart_div_oneLePart`, `leOnePart_eq_one'`, `leOnePart_of_le_one`, `leOnePart_lt`, `leOnePart_le_one'`, `one_lt_ltOnePart`, `oneLePart_inv`, `oneLePart_inf_leOnePart_eq_one`, `inv_le_leOnePart`, `leOnePart_eq_ite_lt`, `Pi.leOnePart_apply`, `leOnePart_eq_one`, `leOnePart_inv`, `leOnePart_max`, `Pi.leOnePart_def`, `leOnePart_one`, `leOnePart_mul_oneLePart`, `div_mabs_eq_inv_leOnePart_sq`, `measurable_leOnePart`, `one_lt_leOnePart`, `oneLePart_mul_leOnePart`, `leOnePart_min`, `one_le_leOnePart`, `leOnePart_eq_inv`, `le_iff_oneLePart_leOnePart`, `leOnePart_eq_ite`, `leOnePart_def`, `one_lt_leOnePart_iff`, `oneLePart_leOnePart_inj`, `leOnePart_eq_inv'`, `mabs_div_eq_leOnePart_sq`, `oneLePart_div_leOnePart`, `Measurable.leOnePart`, `one_lt_ltOnePart_iff`, `leOnePart_anti`
`instNegPart` 📖	CompOp	51 math math: `negPart_nonpos`, `Measurable.negPart`, `negPart_eq_zero'`, `posPart_negPart_inj`, `negPart_eq_neg'`, `Pi.negPart_apply`, `negPart_sub_posPart`, `CFC.negPart_algebraMap`, `negPart_anti`, `negPart_max`, `ValueDistribution.logCounting_top`, `negPart_pos_iff`, `le_iff_posPart_negPart`, `MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_right`, `MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_left`, `negPart_eq_ite`, `posPart_sub_negPart`, `negPart_def`, `negPart_of_nonneg`, `Function.locallyFinsuppWithin.negPart_add`, `negPart_lt`, `lipschitzWith_negPart`, `Pi.negPart_def`, `negPart_min`, `neg_le_negPart`, `continuous_negPart`, `negPart_nonpos'`, `negPart_nonneg`, `negPart_zero`, `posPart_inf_negPart_eq_zero`, `sub_abs_eq_neg_two_nsmul_negPart`, `MeromorphicOn.negPart_divisor_add_le_max`, `measurable_negPart`, `negPart_eq_zero`, `posPart_add_negPart`, `Function.locallyFinsuppWithin.nsmul_negPart`, `CFC.negPart_def`, `BoundedContinuousFunction.coe_negPart`, `MeromorphicOn.negPart_divisor_add_le_add`, `negPart_of_nonpos`, `negPart_eq_neg`, `negPart_eq_neg_inf_zero`, `negPart_pos`, `posPart_negPart_injective`, `posPart_neg`, `Function.locallyFinsuppWithin.restrict_negPart`, `Function.locallyFinsuppWithin.negPart_apply`, `abs_sub_eq_two_nsmul_negPart`, `negPart_neg`, `negPart_eq_ite_lt`, `negPart_add_posPart`
`instOneLePart` 📖	CompOp	35 math math: `oneLePart_mono`, `oneLePart_eq_one`, `Pi.oneLePart_apply`, `oneLePart_leOnePart_injective`, `oneLePart_one`, `leOnePart_div_oneLePart`, `oneLePart_max`, `sup_eq_mul_oneLePart_div`, `oneLePart_min`, `oneLePart_eq_ite_lt`, `measurable_oneLePart`, `oneLePart_inv`, `oneLePart_of_one_le`, `le_oneLePart`, `inf_eq_div_oneLePart_div`, `oneLePart_inf_leOnePart_eq_one`, `one_lt_oneLePart`, `Measurable.oneLePart`, `leOnePart_inv`, `leOnePart_mul_oneLePart`, `oneLePart_le_one`, `mabs_mul_eq_oneLePart_sq`, `oneLePart_mul_leOnePart`, `one_lt_oneLePart_iff`, `oneLePart_def`, `le_iff_oneLePart_leOnePart`, `oneLePart_lt`, `oneLePart_of_le_one`, `oneLePart_leOnePart_inj`, `oneLePart_eq_self`, `Pi.oneLePart_def`, `oneLePart_eq_ite`, `oneLePart_div_leOnePart`, `mul_mabs_eq_oneLePart_sq`, `one_le_oneLePart`
`instPosPart` 📖	CompOp	50 math math: `ValueDistribution.logCounting_zero`, `posPart_max`, `inf_eq_sub_posPart_sub`, `posPart_eq_self`, `posPart_negPart_inj`, `negPart_sub_posPart`, `add_abs_eq_two_nsmul_posPart`, `Function.locallyFinsuppWithin.nsmul_posPart`, `posPart_of_nonpos`, `le_iff_posPart_negPart`, `BoundedContinuousFunction.coe_posPart`, `Function.locallyFinsuppWithin.posPart_add`, `posPart_nonneg`, `abs_add_eq_two_nsmul_posPart`, `posPart_zero`, `MeasureTheory.crossing_pos_eq`, `MeasureTheory.Submartingale.pos`, `posPart_nonpos`, `posPart_def`, `posPart_pos_iff`, `posPart_eq_ite`, `posPart_sub_negPart`, `MeasureTheory.Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part`, `posPart_pos`, `Function.locallyFinsuppWithin.posPart_apply`, `Measurable.posPart`, `posPart_lt`, `Function.locallyFinsuppWithin.restrict_posPart`, `posPart_inf_negPart_eq_zero`, `posPart_add_negPart`, `Pi.posPart_def`, `CFC.posPart_algebraMap`, `Pi.posPart_apply`, `posPart_mono`, `CFC.posPart_def`, `le_posPart`, `posPart_negPart_injective`, `continuous_posPart`, `posPart_neg`, `posPart_eq_zero`, `lipschitzWith_posPart`, `ValueDistribution.logCounting_coe`, `MeasureTheory.upcrossingsBefore_pos_eq`, `sup_eq_add_posPart_sub`, `negPart_neg`, `posPart_of_nonneg`, `posPart_min`, `measurable_posPart`, `posPart_eq_ite_lt`, `negPart_add_posPart`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_add_eq_two_nsmul_posPart` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `abs` `AddMonoid.toNatSMul` `PosPart.posPart` `instPosPart`	—	`two_nsmul` `add_add_sub_cancel` `posPart_add_negPart` `covariant_swap_add_of_covariant_add` `posPart_sub_negPart`
`abs_sub_eq_two_nsmul_negPart` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `abs` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `NegPart.negPart` `instNegPart`	—	`two_nsmul` `add_sub_sub_cancel` `posPart_add_negPart` `covariant_swap_add_of_covariant_add` `posPart_sub_negPart`
`add_abs_eq_two_nsmul_posPart` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `abs` `AddMonoid.toNatSMul` `PosPart.posPart` `instPosPart`	—	`add_comm` `abs_add_eq_two_nsmul_posPart`
`div_mabs_eq_inv_leOnePart_sq` 📖	mathematical	—	`DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `mabs` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `LeOnePart.leOnePart` `instLeOnePart`	—	`mabs_div_eq_leOnePart_sq` `inv_div`
`inf_eq_div_oneLePart_div` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `OneLePart.oneLePart` `instOneLePart`	—	`div_sup` `covariant_swap_mul_of_covariant_mul` `div_div_cancel` `div_one` `inf_comm`
`inf_eq_sub_posPart_sub` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `PosPart.posPart` `instPosPart`	—	`sub_sup` `covariant_swap_add_of_covariant_add` `sub_sub_cancel` `sub_zero` `inf_comm`
`inv_le_leOnePart` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `LeOnePart.leOnePart` `instLeOnePart`	—	`le_sup_left`
`leOnePart_anti` 📖	mathematical	—	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `LeOnePart.leOnePart` `instLeOnePart`	—	`sup_le_sup_right` `inv_le_inv_iff`
`leOnePart_def` 📖	mathematical	—	`LeOnePart.leOnePart` `instLeOnePart` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `InvOneClass.toOne`	—	—
`leOnePart_div_oneLePart` 📖	mathematical	—	`DivInvMonoid.toDiv` `Group.toDivInvMonoid` `LeOnePart.leOnePart` `instLeOnePart` `OneLePart.oneLePart` `instOneLePart` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`inv_div` `oneLePart_div_leOnePart`
`leOnePart_eq_inv` 📖	mathematical	—	`LeOnePart.leOnePart` `instLeOnePart` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `InvOneClass.toOne`	—	—
`leOnePart_eq_inv'` 📖	mathematical	—	`LeOnePart.leOnePart` `instLeOnePart` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `InvOneClass.toOne`	—	`sup_eq_left`
`leOnePart_eq_inv_inf_one` 📖	mathematical	—	`LeOnePart.leOnePart` `instLeOnePart` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `InvOneClass.toOne`	—	`leOnePart_def` `inv_sup` `inv_inv` `inv_one`
`leOnePart_eq_ite` 📖	mathematical	—	`LeOnePart.leOnePart` `instLeOnePart` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `LinearOrder.toDecidableLE` `InvOneClass.toInv`	—	`leOnePart_def` `maxDefault.eq_1` `sup_eq_maxDefault` `LE.total` `sup_comm`
`leOnePart_eq_ite_lt` 📖	mathematical	—	`LeOnePart.leOnePart` `instLeOnePart` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `LinearOrder.toDecidableLT` `InvOneClass.toInv`	—	—
`leOnePart_eq_one` 📖	mathematical	—	`LeOnePart.leOnePart` `instLeOnePart` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	—
`leOnePart_eq_one'` 📖	mathematical	—	`LeOnePart.leOnePart` `instLeOnePart` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `InvOneClass.toInv`	—	`sup_eq_right`
`leOnePart_inv` 📖	mathematical	—	`LeOnePart.leOnePart` `instLeOnePart` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `OneLePart.oneLePart` `instOneLePart`	—	`inv_inv`
`leOnePart_le_one` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `LeOnePart.leOnePart` `instLeOnePart` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`leOnePart_le_one'` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `LeOnePart.leOnePart` `instLeOnePart` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `InvOneClass.toInv`	—	—
`leOnePart_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LeOnePart.leOnePart` `instLeOnePart` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `InvOneClass.toOne`	—	`sup_lt_iff` `inv_lt'` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `LeftCancelSemigroup.toIsLeftCancelMul` `IsRightCancelMul.mulRightStrictMono_of_mulRightMono` `RightCancelSemigroup.toIsRightCancelMul`
`leOnePart_max` 📖	mathematical	—	`LeOnePart.leOnePart` `instLeOnePart` `DistribLattice.toLattice` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`inv_sup` `sup_inf_right`
`leOnePart_min` 📖	mathematical	—	`LeOnePart.leOnePart` `instLeOnePart` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`inv_inf` `sup_sup_distrib_right` `sup_of_le_right` `sup_of_le_left`
`leOnePart_mul_oneLePart` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LeOnePart.leOnePart` `instLeOnePart` `OneLePart.oneLePart` `instOneLePart` `mabs`	—	`oneLePart_def` `mul_sup` `mul_one` `leOnePart_def` `sup_mul` `one_mul` `inv_mul_cancel` `sup_assoc` `sup_eq_right` `le_sup_right` `sup_eq_left` `one_le_mabs`
`leOnePart_of_le_one` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`LeOnePart.leOnePart` `instLeOnePart` `InvOneClass.toInv`	—	`leOnePart_eq_inv`
`leOnePart_of_one_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`LeOnePart.leOnePart` `instLeOnePart`	—	`leOnePart_eq_one`
`leOnePart_one` 📖	mathematical	—	`LeOnePart.leOnePart` `instLeOnePart` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`inv_one` `sup_of_le_left`
`le_iff_oneLePart_leOnePart` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `OneLePart.oneLePart` `instOneLePart` `CommGroup.toGroup` `LeOnePart.leOnePart` `instLeOnePart`	—	`oneLePart_mono` `leOnePart_anti` `covariant_swap_mul_of_covariant_mul` `oneLePart_div_leOnePart` `div_le_div''`
`le_iff_posPart_negPart` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `PosPart.posPart` `instPosPart` `AddCommGroup.toAddGroup` `NegPart.negPart` `instNegPart`	—	`posPart_mono` `negPart_anti` `covariant_swap_add_of_covariant_add` `posPart_sub_negPart` `sub_le_sub`
`le_oneLePart` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `OneLePart.oneLePart` `instOneLePart`	—	`le_sup_left`
`le_posPart` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `PosPart.posPart` `instPosPart`	—	`le_sup_left`
`mabs_div_eq_leOnePart_sq` 📖	mathematical	—	`DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup` `mabs` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `LeOnePart.leOnePart` `instLeOnePart`	—	`sq` `mul_div_div_cancel` `oneLePart_mul_leOnePart` `covariant_swap_mul_of_covariant_mul` `oneLePart_div_leOnePart`
`mabs_mul_eq_oneLePart_sq` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `mabs` `Monoid.toNatPow` `OneLePart.oneLePart` `instOneLePart`	—	`sq` `mul_mul_div_cancel` `oneLePart_mul_leOnePart` `covariant_swap_mul_of_covariant_mul` `oneLePart_div_leOnePart`
`mul_mabs_eq_oneLePart_sq` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `mabs` `Monoid.toNatPow` `OneLePart.oneLePart` `instOneLePart`	—	`mul_comm` `mabs_mul_eq_oneLePart_sq`
`negPart_add_posPart` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegPart.negPart` `instNegPart` `PosPart.posPart` `instPosPart` `abs`	—	`posPart_def` `add_sup` `add_zero` `negPart_def` `sup_add` `zero_add` `neg_add_cancel` `sup_assoc` `sup_eq_right` `le_sup_right` `sup_eq_left` `abs_nonneg`
`negPart_anti` 📖	mathematical	—	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegPart.negPart` `instNegPart`	—	`sup_le_sup_right` `neg_le_neg_iff`
`negPart_def` 📖	mathematical	—	`NegPart.negPart` `instNegPart` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `NegZeroClass.toZero`	—	—
`negPart_eq_ite` 📖	mathematical	—	`NegPart.negPart` `instNegPart` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `LinearOrder.toDecidableLE` `NegZeroClass.toNeg`	—	`neg_nonneg` `negPart_def` `maxDefault.eq_1` `sup_eq_maxDefault` `LE.total` `sup_comm`
`negPart_eq_ite_lt` 📖	mathematical	—	`NegPart.negPart` `instNegPart` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `LinearOrder.toDecidableLT` `NegZeroClass.toNeg`	—	—
`negPart_eq_neg` 📖	mathematical	—	`NegPart.negPart` `instNegPart` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegZeroClass.toZero`	—	`sup_eq_left` `Left.nonneg_neg_iff`
`negPart_eq_neg'` 📖	mathematical	—	`NegPart.negPart` `instNegPart` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegZeroClass.toZero`	—	`sup_eq_left`
`negPart_eq_neg_inf_zero` 📖	mathematical	—	`NegPart.negPart` `instNegPart` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `NegZeroClass.toZero`	—	`negPart_def` `neg_sup` `neg_neg` `neg_zero`
`negPart_eq_zero` 📖	mathematical	—	`NegPart.negPart` `instNegPart` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	`negPart_eq_zero'` `Left.neg_nonpos_iff`
`negPart_eq_zero'` 📖	mathematical	—	`NegPart.negPart` `instNegPart` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegZeroClass.toNeg`	—	`sup_eq_right`
`negPart_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegPart.negPart` `instNegPart` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `NegZeroClass.toZero`	—	`sup_lt_iff` `neg_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd`
`negPart_max` 📖	mathematical	—	`NegPart.negPart` `instNegPart` `DistribLattice.toLattice` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`neg_sup` `sup_inf_right`
`negPart_min` 📖	mathematical	—	`NegPart.negPart` `instNegPart` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`neg_inf` `sup_sup_distrib_right` `sup_of_le_right` `le_sup_right` `sup_of_le_left`
`negPart_neg` 📖	mathematical	—	`NegPart.negPart` `instNegPart` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `PosPart.posPart` `instPosPart`	—	`neg_neg`
`negPart_nonneg` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `NegPart.negPart` `instNegPart`	—	`le_sup_right`
`negPart_nonpos` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegPart.negPart` `instNegPart` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`sup_le_iff` `Left.neg_nonpos_iff` `le_refl`
`negPart_nonpos'` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegPart.negPart` `instNegPart` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `NegZeroClass.toNeg`	—	`sup_le_iff` `le_refl`
`negPart_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`NegPart.negPart` `instNegPart`	—	`negPart_eq_zero`
`negPart_of_nonpos` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`NegPart.negPart` `instNegPart` `NegZeroClass.toNeg`	—	`negPart_eq_neg`
`negPart_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`NegPart.negPart` `instNegPart`	—	`negPart_eq_neg` `LT.lt.le` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`negPart_pos_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `NegPart.negPart` `instNegPart`	—	`lt_iff_lt_of_le_iff_le` `LE.le.ge_iff_eq'` `negPart_nonneg` `negPart_eq_zero`
`negPart_sub_posPart` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NegPart.negPart` `instNegPart` `PosPart.posPart` `instPosPart` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`neg_sub` `posPart_sub_negPart`
`negPart_zero` 📖	mathematical	—	`NegPart.negPart` `instNegPart` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`neg_zero` `sup_of_le_left` `le_refl`
`neg_le_negPart` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `NegPart.negPart` `instNegPart`	—	`le_sup_left`
`oneLePart_def` 📖	mathematical	—	`OneLePart.oneLePart` `instOneLePart` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`oneLePart_div_leOnePart` 📖	mathematical	—	`DivInvMonoid.toDiv` `Group.toDivInvMonoid` `OneLePart.oneLePart` `instOneLePart` `LeOnePart.leOnePart` `instLeOnePart`	—	`div_eq_mul_inv` `mul_inv_eq_iff_eq_mul` `leOnePart_def` `mul_sup` `mul_one` `mul_inv_cancel` `sup_comm` `oneLePart_def`
`oneLePart_eq_ite` 📖	mathematical	—	`OneLePart.oneLePart` `instOneLePart` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `LinearOrder.toDecidableLE`	—	`oneLePart_def` `maxDefault.eq_1` `sup_eq_maxDefault` `LE.total` `sup_comm`
`oneLePart_eq_ite_lt` 📖	mathematical	—	`OneLePart.oneLePart` `instOneLePart` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `LinearOrder.toDecidableLT`	—	—
`oneLePart_eq_one` 📖	mathematical	—	`OneLePart.oneLePart` `instOneLePart` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	`sup_eq_right`
`oneLePart_eq_self` 📖	mathematical	—	`OneLePart.oneLePart` `instOneLePart` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`sup_eq_left`
`oneLePart_inf_leOnePart_eq_one` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `OneLePart.oneLePart` `instOneLePart` `LeOnePart.leOnePart` `instLeOnePart` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`RightCancelSemigroup.toIsRightCancelMul` `inf_mul` `one_mul` `mul_inv_cancel` `div_eq_mul_inv` `oneLePart_div_leOnePart` `leOnePart_eq_inv_inf_one` `inv_inv`
`oneLePart_inv` 📖	mathematical	—	`OneLePart.oneLePart` `instOneLePart` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `LeOnePart.leOnePart` `instLeOnePart`	—	—
`oneLePart_leOnePart_inj` 📖	mathematical	—	`OneLePart.oneLePart` `instOneLePart` `LeOnePart.leOnePart` `instLeOnePart`	—	`oneLePart_leOnePart_injective`
`oneLePart_leOnePart_injective` 📖	mathematical	—	`OneLePart.oneLePart` `instOneLePart` `LeOnePart.leOnePart` `instLeOnePart`	—	`oneLePart_div_leOnePart`
`oneLePart_le_one` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `OneLePart.oneLePart` `instOneLePart` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`oneLePart_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `OneLePart.oneLePart` `instOneLePart` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`sup_lt_iff`
`oneLePart_max` 📖	mathematical	—	`OneLePart.oneLePart` `instOneLePart` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`sup_sup_distrib_right` `sup_of_le_right` `sup_of_le_left`
`oneLePart_min` 📖	mathematical	—	`OneLePart.oneLePart` `instOneLePart` `DistribLattice.toLattice` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`sup_inf_right`
`oneLePart_mono` 📖	mathematical	—	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `OneLePart.oneLePart` `instOneLePart`	—	`sup_le_sup_right`
`oneLePart_mul_leOnePart` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `OneLePart.oneLePart` `instOneLePart` `LeOnePart.leOnePart` `instLeOnePart` `mabs`	—	`oneLePart_def` `sup_mul` `one_mul` `leOnePart_def` `mul_sup` `mul_one` `mul_inv_cancel` `sup_assoc` `sup_eq_right` `le_sup_right` `sup_eq_left` `one_le_mabs`
`oneLePart_of_le_one` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`OneLePart.oneLePart` `instOneLePart`	—	`oneLePart_eq_one`
`oneLePart_of_one_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`OneLePart.oneLePart` `instOneLePart`	—	`oneLePart_eq_self`
`oneLePart_of_one_lt_oneLePart` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `OneLePart.oneLePart` `instOneLePart`	—	—	`oneLePart_eq_self` `LT.lt.le` `not_le` `right_lt_sup` `oneLePart_def`
`oneLePart_one` 📖	mathematical	—	`OneLePart.oneLePart` `instOneLePart` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`sup_idem`
`one_le_leOnePart` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `LeOnePart.leOnePart` `instLeOnePart`	—	`le_sup_right`
`one_le_oneLePart` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `OneLePart.oneLePart` `instOneLePart`	—	`le_sup_right`
`one_lt_leOnePart` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`LeOnePart.leOnePart` `instLeOnePart`	—	`leOnePart_eq_inv` `LT.lt.le` `one_lt_inv'` `IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono` `LeftCancelSemigroup.toIsLeftCancelMul`
`one_lt_leOnePart_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `LeOnePart.leOnePart` `instLeOnePart`	—	`lt_iff_lt_of_le_iff_le` `LE.le.ge_iff_eq'` `one_le_leOnePart` `leOnePart_eq_one`
`one_lt_ltOnePart` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`LeOnePart.leOnePart` `instLeOnePart`	—	`one_lt_leOnePart`
`one_lt_ltOnePart_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `LeOnePart.leOnePart` `instLeOnePart`	—	`one_lt_leOnePart_iff`
`one_lt_oneLePart` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`OneLePart.oneLePart` `instOneLePart`	—	`oneLePart_eq_self` `LT.lt.le`
`one_lt_oneLePart_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `OneLePart.oneLePart` `instOneLePart`	—	`lt_iff_lt_of_le_iff_le` `LE.le.ge_iff_eq'` `one_le_oneLePart` `oneLePart_eq_one`
`posPart_add_negPart` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `PosPart.posPart` `instPosPart` `NegPart.negPart` `instNegPart` `abs`	—	`posPart_def` `sup_add` `zero_add` `negPart_def` `add_sup` `add_zero` `add_neg_cancel` `sup_assoc` `sup_eq_right` `le_sup_right` `sup_eq_left` `abs_nonneg`
`posPart_def` 📖	mathematical	—	`PosPart.posPart` `instPosPart` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`posPart_eq_ite` 📖	mathematical	—	`PosPart.posPart` `instPosPart` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `LinearOrder.toDecidableLE`	—	`posPart_def` `maxDefault.eq_1` `sup_eq_maxDefault` `LE.total` `sup_comm`
`posPart_eq_ite_lt` 📖	mathematical	—	`PosPart.posPart` `instPosPart` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `LinearOrder.toDecidableLT`	—	—
`posPart_eq_of_posPart_pos` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `PosPart.posPart` `instPosPart`	—	—	`posPart_eq_self` `LT.lt.le` `not_le` `right_lt_sup` `posPart_def`
`posPart_eq_self` 📖	mathematical	—	`PosPart.posPart` `instPosPart` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`sup_eq_left`
`posPart_eq_zero` 📖	mathematical	—	`PosPart.posPart` `instPosPart` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	`sup_eq_right`
`posPart_inf_negPart_eq_zero` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `PosPart.posPart` `instPosPart` `NegPart.negPart` `instNegPart` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `inf_add` `zero_add` `add_neg_cancel` `sub_eq_add_neg` `posPart_sub_negPart` `negPart_eq_neg_inf_zero` `neg_neg`
`posPart_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `PosPart.posPart` `instPosPart` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`sup_lt_iff`
`posPart_max` 📖	mathematical	—	`PosPart.posPart` `instPosPart` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`sup_sup_distrib_right` `sup_of_le_right` `le_sup_right` `sup_of_le_left`
`posPart_min` 📖	mathematical	—	`PosPart.posPart` `instPosPart` `DistribLattice.toLattice` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`sup_inf_right`
`posPart_mono` 📖	mathematical	—	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `PosPart.posPart` `instPosPart`	—	`sup_le_sup_right`
`posPart_neg` 📖	mathematical	—	`PosPart.posPart` `instPosPart` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `NegPart.negPart` `instNegPart`	—	—
`posPart_negPart_inj` 📖	mathematical	—	`PosPart.posPart` `instPosPart` `NegPart.negPart` `instNegPart`	—	`posPart_negPart_injective`
`posPart_negPart_injective` 📖	mathematical	—	`PosPart.posPart` `instPosPart` `NegPart.negPart` `instNegPart`	—	`posPart_sub_negPart`
`posPart_nonneg` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `PosPart.posPart` `instPosPart`	—	`le_sup_right`
`posPart_nonpos` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `PosPart.posPart` `instPosPart` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`sup_le_iff` `le_refl`
`posPart_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`PosPart.posPart` `instPosPart`	—	`posPart_eq_self`
`posPart_of_nonpos` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`PosPart.posPart` `instPosPart`	—	`posPart_eq_zero`
`posPart_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`PosPart.posPart` `instPosPart`	—	`posPart_eq_self` `LT.lt.le`
`posPart_pos_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `PosPart.posPart` `instPosPart`	—	`lt_iff_lt_of_le_iff_le` `LE.le.ge_iff_eq'` `posPart_nonneg` `posPart_eq_zero`
`posPart_sub_negPart` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `PosPart.posPart` `instPosPart` `NegPart.negPart` `instNegPart`	—	`sub_eq_add_neg` `add_neg_eq_iff_eq_add` `negPart_def` `add_sup` `add_zero` `add_neg_cancel` `sup_comm` `posPart_def`
`posPart_zero` 📖	mathematical	—	`PosPart.posPart` `instPosPart` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`sup_idem`
`sub_abs_eq_neg_two_nsmul_negPart` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `abs` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `NegPart.negPart` `instNegPart`	—	`abs_sub_eq_two_nsmul_negPart` `neg_sub`
`sup_eq_add_posPart_sub` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `PosPart.posPart` `instPosPart` `SubNegMonoid.toSub`	—	`add_sup` `add_sub_cancel` `add_zero`
`sup_eq_mul_oneLePart_div` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `OneLePart.oneLePart` `instOneLePart` `DivInvMonoid.toDiv`	—	`mul_sup` `mul_div_cancel` `mul_one`

---

← Back to Index