Inv

📁 Source: Mathlib/Data/EReal/Inv.lean

Statistics

Metric	Count
Definitions `abs`, `instCommMonoidWithZero`, `instDivInvMonoid`, `instDivInvOneMonoid`, `instInv`, `inv`, `evalERealDiv`, `evalERealInv`	8
Theorems `abs_bot`, `abs_coe_lt_top`, `abs_def`, `abs_eq_zero_iff`, `abs_mul`, `abs_mul_sign`, `abs_neg`, `abs_top`, `abs_zero`, `add_div_of_nonneg_right`, `antitone_div_right_of_nonpos`, `bot_div_of_neg_ne_bot`, `bot_div_of_pos_ne_top`, `bot_lt_inv`, `coe_abs`, `coe_coe_sign`, `coe_div`, `coe_ennreal_pow`, `coe_inv`, `coe_pow`, `div_bot`, `div_div`, `div_eq_iff`, `div_eq_inv_mul`, `div_le_div_right_of_nonneg`, `div_le_div_right_of_nonpos`, `div_le_iff_le_mul`, `div_lt_div_right_of_neg`, `div_lt_div_right_of_pos`, `div_lt_iff`, `div_mul_cancel`, `div_mul_div_comm`, `div_nonneg`, `div_nonneg_of_nonpos_of_nonpos`, `div_nonpos_of_nonneg_of_nonpos`, `div_nonpos_of_nonpos_of_nonneg`, `div_pos`, `div_right_distrib_of_nonneg`, `div_self`, `div_top`, `div_zero`, `exists_nat_ge_mul`, `instMulPosMono`, `instMulPosReflectLT`, `instPosMulMono`, `instPosMulReflectLT`, `inv_bot`, `inv_inv`, `inv_lt_top`, `inv_neg`, `inv_neg_of_neg_ne_bot`, `inv_nonneg_of_nonneg`, `inv_nonpos_of_nonpos`, `inv_pos_of_pos_ne_top`, `inv_strictAntiOn`, `inv_top`, `inv_zero`, `le_div_iff_mul_le`, `le_iff_sign`, `le_mul_of_forall_lt`, `lt_div_iff`, `max_neg_neg`, `min_neg_neg`, `monotone_div_right_of_nonneg`, `mul_div`, `mul_div_cancel`, `mul_div_left_comm`, `mul_div_mul_cancel`, `mul_div_right`, `mul_inv`, `mul_le_mul_of_nonpos_right`, `mul_le_of_forall_lt_of_nonneg`, `natCast_div_le`, `sign_bot`, `sign_coe`, `sign_eq_and_abs_eq_iff_eq`, `sign_mul`, `sign_mul_abs`, `sign_mul_inv_abs`, `sign_mul_inv_abs'`, `sign_neg`, `sign_top`, `strictAnti_div_right_of_neg`, `strictMono_div_right_of_pos`, `top_div_of_neg_ne_bot`, `top_div_of_pos_ne_top`, `zero_div`	87
Total	95

EReal

Definitions

Name	Category	Theorems
`abs` 📖	CompOp	15 math math: `abs_neg`, `sign_eq_and_abs_eq_iff_eq`, `abs_eq_zero_iff`, `abs_mul_sign`, `abs_top`, `abs_coe_lt_top`, `abs_mul`, `abs_zero`, `le_iff_sign`, `abs_def`, `sign_mul_inv_abs`, `sign_mul_abs`, `coe_abs`, `abs_bot`, `sign_mul_inv_abs'`
`instCommMonoidWithZero` 📖	CompOp	2 math math: `coe_ennreal_pow`, `coe_pow`
`instDivInvMonoid` 📖	CompOp	99 math math: `LinearGrowth.linearGrowthSup_zero`, `LinearGrowth.linearGrowthSup_top`, `div_eq_inv_mul`, `LinearGrowth.linearGrowthInf_add_le'`, `LinearGrowth.le_linearGrowthSup_add`, `LinearGrowth.linearGrowthSup_add_le`, `div_le_div_right_of_nonneg`, `top_div_of_neg_ne_bot`, `div_mul_div_comm`, `LinearGrowth.le_linearGrowthSup_add'`, `LinearGrowth.linearGrowthInf_bot`, `strictMono_div_right_of_pos`, `LinearGrowth.linearGrowthSup_bot`, `LinearGrowth.linearGrowthInf_biInf`, `ExpGrowth.expGrowthSup_def`, `Eventually.le_linearGrowthInf`, `bot_div_of_neg_ne_bot`, `LinearGrowth.linearGrowthInf_top`, `mul_div_mul_cancel`, `LinearGrowth.linearGrowthInf_const_mul_self`, `strictAnti_div_right_of_neg`, `LinearGrowth.linearGrowthInf_zero`, `Eventually.linearGrowthSup_le`, `lt_div_iff`, `LinearGrowth.linearGrowthSup_le_of_eventually_le`, `LinearGrowth.linearGrowthSup_biSup`, `LinearGrowth.linearGrowthSup_inv`, `LinearGrowth.linearGrowthInf_const`, `mul_div`, `LinearGrowth.linearGrowthSup_le_iff`, `ExpGrowth.le_expGrowthInf_comp`, `monotone_div_right_of_nonneg`, `LinearGrowth.linearGrowthSup_const_mul_self`, `tendsto_const_div_atTop_nhds_zero_nat`, `LinearGrowth.linearGrowthSup_sup`, `LinearGrowth.linearGrowthInf_inf`, `div_le_div_right_of_nonpos`, `div_zero`, `Dynamics.IsDynCoverOf.coverEntropyEntourage_le_log_card_div`, `LinearGrowth.linearGrowthSup_eventually_monotone`, `LinearGrowth.linearGrowthSup_const`, `LinearGrowth.linearGrowthInf_natCast_nonneg`, `LinearGrowth.linearGrowthSup_comp_nonneg`, `Dynamics.coverEntropyEntourage_le_log_coverMincard_div`, `Monotone.linearGrowthInf_nonneg`, `ExpGrowth.expGrowthSup_comp_le`, `div_self`, `LinearGrowth.linearGrowthInf_eventually_monotone`, `Monotone.expGrowthInf_comp_le`, `top_div_of_pos_ne_top`, `div_lt_div_right_of_pos`, `div_lt_iff`, `LinearGrowth.linearGrowthInf_iInf`, `LinearGrowth.linearGrowthInf_monotone`, `div_pos`, `LinearGrowth.linearGrowthSup_iSup`, `LinearGrowth.linearGrowthInf_comp_nonneg`, `div_top`, `mul_div_cancel`, `bot_div_of_pos_ne_top`, `LinearGrowth.le_linearGrowthInf_iff`, `div_nonpos_of_nonpos_of_nonneg`, `ExpGrowth.expGrowthInf_def`, `add_div_of_nonneg_right`, `LinearGrowth.linearGrowthInf_le_of_eventually_le`, `LinearGrowth.linearGrowthInf_le_iff`, `LinearGrowth.linearGrowthSup_comp_le`, `Monotone.linearGrowthInf_comp_le`, `mul_div_left_comm`, `Monotone.linearGrowthInf_comp_mul`, `zero_div`, `div_nonneg`, `LinearGrowth.linearGrowthInf_add_le`, `Frequently.linearGrowthInf_le`, `div_mul_cancel`, `natCast_div_le`, `mul_div_right`, `coe_div`, `Monotone.linearGrowthSup_nonneg`, `div_right_distrib_of_nonneg`, `Monotone.linearGrowthSup_comp_mul`, `Monotone.le_linearGrowthSup_comp`, `div_le_iff_le_mul`, `div_eq_iff`, `div_lt_div_right_of_neg`, `div_nonneg_of_nonpos_of_nonpos`, `div_nonpos_of_nonneg_of_nonpos`, `LinearGrowth.linearGrowthSup_monotone`, `LinearGrowth.linearGrowthInf_le_linearGrowthSup_of_frequently_le`, `LinearGrowth.le_linearGrowthInf_comp`, `LinearGrowth.le_linearGrowthSup_iff`, `le_div_iff_mul_le`, `div_div`, `antitone_div_right_of_nonpos`, `div_bot`, `LinearGrowth.le_linearGrowthInf_add`, `Frequently.le_linearGrowthSup`, `LinearGrowth.linearGrowthInf_neg`, `Monotone.le_expGrowthSup_comp`
`instDivInvOneMonoid` 📖	CompOp	—
`instInv` 📖	CompOp	17 math math: `inv_strictAntiOn`, `div_eq_inv_mul`, `inv_nonneg_of_nonneg`, `inv_inv`, `inv_nonpos_of_nonpos`, `inv_neg`, `bot_lt_inv`, `inv_top`, `inv_bot`, `inv_lt_top`, `inv_neg_of_neg_ne_bot`, `sign_mul_inv_abs`, `coe_inv`, `mul_inv`, `inv_pos_of_pos_ne_top`, `sign_mul_inv_abs'`, `inv_zero`
`inv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_bot` 📖	mathematical	—	`abs` `Bot.bot` `EReal` `instBotEReal` `Top.top` `ENNReal` `instTopENNReal`	—	—
`abs_coe_lt_top` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `abs` `Real.toEReal` `Top.top` `instTopENNReal`	—	`ENNReal.ofReal_lt_top`
`abs_def` 📖	mathematical	—	`abs` `Real.toEReal` `ENNReal.ofReal` `abs` `Real` `Real.lattice` `Real.instAddGroup`	—	—
`abs_eq_zero_iff` 📖	mathematical	—	`abs` `ENNReal` `instZeroENNReal` `EReal` `instZeroEReal`	—	`IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`abs_mul` 📖	mathematical	—	`abs` `EReal` `instMul` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`induction₂_symm_neg` `mul_comm` `mul_comm` `neg_mul` `abs_neg` `top_mul_coe_of_pos` `abs_top` `ENNReal.top_mul` `abs_eq_zero_iff` `coe_eq_zero` `LT.lt.ne'` `MulZeroClass.mul_zero` `abs_zero` `abs_mul` `Real.instIsOrderedRing` `ENNReal.ofReal_mul` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`abs_mul_sign` 📖	mathematical	—	`EReal` `instMul` `ENNReal.toEReal` `abs` `SignType.cast` `instZeroEReal` `instOneEReal` `instNeg` `DFunLike.coe` `OrderHom` `SignType` `PartialOrder.toPreorder` `instPartialOrderEReal` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `decidableLT`	—	`mul_comm` `sign_mul_abs`
`abs_neg` 📖	mathematical	—	`abs` `EReal` `instNeg`	—	`abs_def` `coe_neg` `abs_neg`
`abs_top` 📖	mathematical	—	`abs` `Top.top` `EReal` `instTop` `ENNReal` `instTopENNReal`	—	—
`abs_zero` 📖	mathematical	—	`abs` `EReal` `instZeroEReal` `ENNReal` `instZeroENNReal`	—	`abs_eq_zero_iff`
`add_div_of_nonneg_right` 📖	mathematical	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`DivInvMonoid.toDiv` `instDivInvMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal`	—	`right_distrib_of_nonneg_of_ne_top` `inv_nonneg_of_nonneg` `LT.lt.ne` `inv_lt_top`
`antitone_div_right_of_nonpos` 📖	mathematical	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`Antitone` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`neg_neg` `neg_le_neg_iff` `mul_comm` `neg_mul` `inv_neg` `le_neg_of_le_neg` `neg_zero` `div_le_div_right_of_nonneg`
`bot_div_of_neg_ne_bot` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`DivInvMonoid.toDiv` `instDivInvMonoid` `Bot.bot` `instBotEReal` `Top.top` `instTop`	—	`bot_mul_of_neg` `inv_neg_of_neg_ne_bot`
`bot_div_of_pos_ne_top` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`DivInvMonoid.toDiv` `instDivInvMonoid` `Bot.bot` `instBotEReal`	—	`bot_mul_of_pos` `inv_pos_of_pos_ne_top`
`bot_lt_inv` 📖	mathematical	—	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `Bot.bot` `instBotEReal` `instInv`	—	`bot_lt_zero` `inv_bot` `bot_lt_coe` `coe_inv` `inv_top`
`coe_abs` 📖	mathematical	—	`ENNReal.toEReal` `abs` `Real.toEReal` `abs` `Real` `Real.lattice` `Real.instAddGroup`	—	`abs_def` `Real.coe_nnabs` `ENNReal.ofReal_coe_nnreal`
`coe_coe_sign` 📖	mathematical	—	`Real.toEReal` `SignType.cast` `Real` `Real.instZero` `Real.instOne` `Real.instNeg` `EReal` `instZeroEReal` `instOneEReal` `instNeg`	—	—
`coe_div` 📖	mathematical	—	`Real.toEReal` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `EReal` `instDivInvMonoid`	—	—
`coe_ennreal_pow` 📖	mathematical	—	`ENNReal.toEReal` `ENNReal` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `EReal` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	—	`map_pow` `MonoidHom.instMonoidHomClass` `coe_ennreal_one` `coe_ennreal_mul`
`coe_inv` 📖	mathematical	—	`Real.toEReal` `Real` `Real.instInv` `EReal` `instInv`	—	—
`coe_pow` 📖	mathematical	—	`Real.toEReal` `Real` `Monoid.toNatPow` `Real.instMonoid` `EReal` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `instCommMonoidWithZero`	—	`map_pow` `MonoidHom.instMonoidHomClass` `coe_one` `coe_mul`
`div_bot` 📖	mathematical	—	`EReal` `DivInvMonoid.toDiv` `instDivInvMonoid` `Bot.bot` `instBotEReal` `instZeroEReal`	—	`MulZeroClass.mul_zero` `inv_bot`
`div_div` 📖	mathematical	—	`EReal` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul`	—	`mul_assoc` `mul_inv`
`div_eq_iff` 📖	mathematical	—	`EReal` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul`	—	`mul_div_cancel` `mul_comm` `mul_div`
`div_eq_inv_mul` 📖	mathematical	—	`EReal` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul` `instInv`	—	`mul_comm`
`div_le_div_right_of_nonneg` 📖	mathematical	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`DivInvMonoid.toDiv` `instDivInvMonoid`	—	`monotone_div_right_of_nonneg`
`div_le_div_right_of_nonpos` 📖	mathematical	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`DivInvMonoid.toDiv` `instDivInvMonoid`	—	`antitone_div_right_of_nonpos`
`div_le_iff_le_mul` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`Preorder.toLE` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul`	—	`mul_div_cancel` `ne_bot_of_gt` `ne_of_gt` `mul_div` `mul_comm` `StrictMono.le_iff_le` `strictMono_div_right_of_pos`
`div_lt_div_right_of_neg` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`DivInvMonoid.toDiv` `instDivInvMonoid`	—	`strictAnti_div_right_of_neg`
`div_lt_div_right_of_pos` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`DivInvMonoid.toDiv` `instDivInvMonoid`	—	`strictMono_div_right_of_pos`
`div_lt_iff` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`DivInvMonoid.toDiv` `instDivInvMonoid` `instMul`	—	`mul_div_cancel` `ne_bot_of_gt` `ne_of_gt` `mul_div` `mul_comm` `StrictMono.lt_iff_lt` `strictMono_div_right_of_pos`
`div_mul_cancel` 📖	mathematical	—	`EReal` `instMul` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`mul_comm` `mul_div_left_comm` `div_self` `mul_one`
`div_mul_div_comm` 📖	mathematical	—	`EReal` `instMul` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`mul_div` `mul_comm` `div_div` `mul_div_left_comm`
`div_nonneg` 📖	mathematical	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`DivInvMonoid.toDiv` `instDivInvMonoid`	—	`mul_nonneg` `instPosMulMono` `inv_nonneg_of_nonneg`
`div_nonneg_of_nonpos_of_nonpos` 📖	mathematical	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`DivInvMonoid.toDiv` `instDivInvMonoid`	—	`zero_div` `div_le_div_right_of_nonpos`
`div_nonpos_of_nonneg_of_nonpos` 📖	mathematical	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`DivInvMonoid.toDiv` `instDivInvMonoid`	—	`mul_nonpos_of_nonneg_of_nonpos` `instPosMulMono` `inv_nonpos_of_nonpos`
`div_nonpos_of_nonpos_of_nonneg` 📖	mathematical	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`DivInvMonoid.toDiv` `instDivInvMonoid`	—	`mul_nonpos_of_nonpos_of_nonneg` `instMulPosMono` `inv_nonneg_of_nonneg`
`div_pos` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`DivInvMonoid.toDiv` `instDivInvMonoid`	—	`mul_pos` `inv_pos_of_pos_ne_top`
`div_right_distrib_of_nonneg` 📖	mathematical	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`DivInvMonoid.toDiv` `instDivInvMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal`	—	`right_distrib_of_nonneg`
`div_self` 📖	mathematical	—	`EReal` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOneEReal`	—	`coe_toReal` `coe_div` `div_self` `coe_ne_zero` `coe_one`
`div_top` 📖	mathematical	—	`EReal` `DivInvMonoid.toDiv` `instDivInvMonoid` `Top.top` `instTop` `instZeroEReal`	—	`MulZeroClass.mul_zero` `inv_top`
`div_zero` 📖	mathematical	—	`EReal` `DivInvMonoid.toDiv` `instDivInvMonoid` `instZeroEReal`	—	`inv_zero` `MulZeroClass.mul_zero`
`exists_nat_ge_mul` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instMul` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal`	—	`mul_nonpos_iff` `bot_le` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoidEReal` `instZeroLEOneClassEReal` `Nat.cast_zero` `exists_nat_ge` `Real.instIsOrderedRing` `Real.instArchimedean` `coe_coe_eq_natCast` `coe_mul` `coe_le_coe_iff`
`instMulPosMono` 📖	mathematical	—	`MulPosMono` `EReal` `instMul` `instZeroEReal` `PartialOrder.toPreorder` `instPartialOrderEReal`	—	`posMulMono_iff_mulPosMono` `CommMagma.to_isCommutative` `instPosMulMono`
`instMulPosReflectLT` 📖	mathematical	—	`MulPosReflectLT` `EReal` `instMul` `instZeroEReal` `PartialOrder.toPreorder` `instPartialOrderEReal`	—	`MulPosMono.toMulPosReflectLT` `instMulPosMono`
`instPosMulMono` 📖	mathematical	—	`PosMulMono` `EReal` `instMul` `instZeroEReal` `PartialOrder.toPreorder` `instPartialOrderEReal`	—	`posMulMono_iff_covariant_pos` `sign_mul` `sign_pos` `one_mul` `abs_mul` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid`
`instPosMulReflectLT` 📖	mathematical	—	`PosMulReflectLT` `EReal` `instMul` `instZeroEReal` `PartialOrder.toPreorder` `instPartialOrderEReal`	—	`PosMulMono.toPosMulReflectLT` `instPosMulMono`
`inv_bot` 📖	mathematical	—	`EReal` `instInv` `Bot.bot` `instBotEReal` `instZeroEReal`	—	—
`inv_inv` 📖	mathematical	—	`EReal` `instInv`	—	`coe_toReal` `coe_inv` `inv_inv`
`inv_lt_top` 📖	mathematical	—	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `instInv` `Top.top` `instTop`	—	`zero_lt_top` `inv_bot` `coe_lt_top` `coe_inv` `inv_top`
`inv_neg` 📖	mathematical	—	`EReal` `instInv` `instNeg`	—	`neg_bot` `inv_top` `inv_bot` `neg_zero` `coe_inv` `coe_neg` `coe_eq_coe_iff` `inv_neg` `neg_top`
`inv_neg_of_neg_ne_bot` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`instInv`	—	`CanLift.prf` `canLift` `ne_top_of_lt` `coe_inv` `Nat.cast_zero` `inv_lt_zero` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing`
`inv_nonneg_of_nonneg` 📖	mathematical	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`instInv`	—	`coe_inv` `coe_nonneg` `inv_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing`
`inv_nonpos_of_nonpos` 📖	mathematical	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`instInv`	—	`coe_inv` `coe_nonpos` `inv_nonpos` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing`
`inv_pos_of_pos_ne_top` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`instInv`	—	`CanLift.prf` `canLift` `ne_bot_of_gt` `coe_inv` `Nat.cast_zero` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing`
`inv_strictAntiOn` 📖	mathematical	—	`StrictAntiOn` `EReal` `PartialOrder.toPreorder` `instPartialOrderEReal` `instInv` `Set.Ioi` `instZeroEReal`	—	`CanLift.prf` `canLift` `ne_top_of_lt` `ne_bot_of_gt` `inv_pos_of_pos_ne_top` `coe_ne_top` `inv_top` `not_lt_bot` `coe_inv` `coe_lt_coe_iff` `inv_strictAntiOn` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `coe_pos`
`inv_top` 📖	mathematical	—	`EReal` `instInv` `Top.top` `instTop` `instZeroEReal`	—	—
`inv_zero` 📖	mathematical	—	`EReal` `instInv` `instZeroEReal`	—	`GroupWithZero.inv_zero` `coe_zero`
`le_div_iff_mul_le` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`Preorder.toLE` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul`	—	`mul_div_cancel` `ne_bot_of_gt` `ne_of_gt` `mul_div` `mul_comm` `StrictMono.le_iff_le` `strictMono_div_right_of_pos`
`le_iff_sign` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `SignType` `Preorder.toLT` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `DFunLike.coe` `OrderHom` `OrderHom.instFunLike` `SignType.sign` `instZeroEReal` `decidableLT` `SignType.neg` `ENNReal` `ENNReal.instPartialOrder` `abs` `SignType.zero` `SignType.pos`	—	`NeZero.one` `GroupWithZero.toNontrivial` `neg_mul` `one_mul` `sign_mul_abs` `LE.le.lt_or_eq` `OrderHom.monotone` `LT.lt.le` `Monotone.reflect_lt` `MulZeroClass.zero_mul`
`le_mul_of_forall_lt` 📖	—	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal` `Preorder.toLE` `instMul`	—	—	`le_of_forall_gt_imp_ge_of_dense` `instDenselyOrderedEReal` `ne_of_gt` `LT.lt.trans` `Set.mem_Ioo` `LT.lt.ne` `LE.le.trans` `LT.lt.le`
`lt_div_iff` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`DivInvMonoid.toDiv` `instDivInvMonoid` `instMul`	—	`mul_div_cancel` `ne_bot_of_gt` `ne_of_gt` `mul_div` `mul_comm` `StrictMono.lt_iff_lt` `strictMono_div_right_of_pos`
`max_neg_neg` 📖	mathematical	—	`EReal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `instNeg` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`le_total` `sup_of_le_left` `inf_of_le_left` `sup_of_le_right` `inf_of_le_right`
`min_neg_neg` 📖	mathematical	—	`EReal` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `instNeg` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`le_total` `inf_of_le_right` `sup_of_le_right` `inf_of_le_left` `sup_of_le_left`
`monotone_div_right_of_nonneg` 📖	mathematical	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`Monotone` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`mul_le_mul_of_nonneg_right` `instMulPosMono` `inv_nonneg_of_nonneg`
`mul_div` 📖	mathematical	—	`EReal` `instMul` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`mul_assoc`
`mul_div_cancel` 📖	mathematical	—	`EReal` `instMul` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`mul_comm` `div_mul_cancel`
`mul_div_left_comm` 📖	mathematical	—	`EReal` `instMul` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`mul_div` `mul_comm`
`mul_div_mul_cancel` 📖	mathematical	—	`EReal` `DivInvMonoid.toDiv` `instDivInvMonoid` `instMul`	—	`mul_div_right` `div_div` `div_mul_cancel`
`mul_div_right` 📖	mathematical	—	`EReal` `instMul` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`mul_comm` `mul_div`
`mul_inv` 📖	mathematical	—	`EReal` `instInv` `instMul`	—	`induction₂_symm` `mul_comm` `MulZeroClass.mul_zero` `top_mul_of_pos` `coe_pos` `inv_top` `MulZeroClass.zero_mul` `inv_zero` `top_mul_of_neg` `coe_neg'` `inv_bot` `mul_bot_of_pos` `coe_mul` `coe_inv` `mul_inv` `mul_bot_of_neg`
`mul_le_mul_of_nonpos_right` 📖	mathematical	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`instMul`	—	`mul_comm` `neg_le_neg_iff` `neg_mul` `mul_le_mul_of_nonneg_left` `instPosMulMono` `le_neg` `neg_zero`
`mul_le_of_forall_lt_of_nonneg` 📖	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal` `instMul`	—	—	`le_of_forall_lt_imp_le_of_dense` `instDenselyOrderedEReal` `lt_or_ge` `LE.le.trans` `LT.lt.le`
`natCast_div_le` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`coe_coe_eq_natCast` `coe_div` `coe_le_coe_iff` `Nat.cast_div_le` `Real.instIsStrictOrderedRing`
`sign_bot` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `EReal` `SignType` `PartialOrder.toPreorder` `instPartialOrderEReal` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `instZeroEReal` `decidableLT` `Bot.bot` `instBotEReal` `SignType.instNeg` `SignType.instOne`	—	—
`sign_coe` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `EReal` `SignType` `PartialOrder.toPreorder` `instPartialOrderEReal` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `instZeroEReal` `decidableLT` `Real.toEReal` `Real` `Real.instPreorder` `Real.instZero` `Real.decidableLT`	—	—
`sign_eq_and_abs_eq_iff_eq` 📖	mathematical	—	`abs` `DFunLike.coe` `OrderHom` `EReal` `SignType` `PartialOrder.toPreorder` `instPartialOrderEReal` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `instZeroEReal` `decidableLT`	—	`sign_mul_abs`
`sign_mul` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `EReal` `SignType` `PartialOrder.toPreorder` `instPartialOrderEReal` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `instZeroEReal` `decidableLT` `instMul` `SignType.instMul`	—	`induction₂_symm_neg` `mul_comm` `mul_comm` `neg_mul` `sign_neg` `top_mul_coe_of_pos` `sign_top` `one_mul` `sign_pos` `coe_pos` `MulZeroClass.mul_zero` `sign_zero` `sign_coe` `sign_mul` `Real.instIsStrictOrderedRing`
`sign_mul_abs` 📖	mathematical	—	`EReal` `instMul` `SignType.cast` `instZeroEReal` `instOneEReal` `instNeg` `DFunLike.coe` `OrderHom` `SignType` `PartialOrder.toPreorder` `instPartialOrderEReal` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `decidableLT` `ENNReal.toEReal` `abs`	—	`sign_neg` `neg_mul` `one_mul` `sign_pos` `sign_coe` `coe_abs` `coe_coe_sign` `coe_mul` `sign_mul_abs` `Real.instIsStrictOrderedRing`
`sign_mul_inv_abs` 📖	mathematical	—	`EReal` `instMul` `SignType.cast` `instZeroEReal` `instOneEReal` `instNeg` `DFunLike.coe` `OrderHom` `SignType` `PartialOrder.toPreorder` `instPartialOrderEReal` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `decidableLT` `instInv` `ENNReal.toEReal` `abs`	—	`sign_neg` `MulZeroClass.mul_zero` `lt_trichotomy` `sign_coe` `SignType.coe_neg_one` `neg_one_mul` `inv_neg` `abs_def` `coe_ennreal_ofReal` `max_eq_left` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `coe_neg` `abs_of_neg` `neg_neg` `coe_zero` `sign_zero` `SignType.coe_zero` `abs_zero` `coe_ennreal_zero` `inv_zero` `sign_pos` `SignType.coe_one` `one_mul` `abs_of_pos`
`sign_mul_inv_abs'` 📖	mathematical	—	`EReal` `instMul` `SignType.cast` `instZeroEReal` `instOneEReal` `instNeg` `DFunLike.coe` `OrderHom` `SignType` `PartialOrder.toPreorder` `instPartialOrderEReal` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `decidableLT` `ENNReal.toEReal` `ENNReal` `ENNReal.instInv` `abs` `instInv`	—	`sign_neg` `ENNReal.inv_top` `MulZeroClass.mul_zero` `lt_trichotomy` `sign_coe` `SignType.coe_neg_one` `neg_one_mul` `abs_def` `ENNReal.ofReal_inv_of_pos` `abs_pos_of_neg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `coe_ennreal_ofReal` `max_eq_left` `inv_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `abs_nonneg` `covariant_swap_add_of_covariant_add` `coe_neg` `coe_inv` `abs_of_neg` `inv_neg` `neg_neg` `sign_zero` `abs_zero` `ENNReal.inv_zero` `MulZeroClass.zero_mul` `inv_zero` `sign_pos` `SignType.coe_one` `one_mul` `abs_pos_of_pos` `abs_of_pos`
`sign_neg` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `EReal` `SignType` `PartialOrder.toPreorder` `instPartialOrderEReal` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `instZeroEReal` `decidableLT` `instNeg` `SignType.instNeg`	—	`coe_neg` `sign_coe` `Left.sign_neg` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`sign_top` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `EReal` `SignType` `PartialOrder.toPreorder` `instPartialOrderEReal` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `instZeroEReal` `decidableLT` `Top.top` `instTop` `SignType.instOne`	—	—
`strictAnti_div_right_of_neg` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`StrictAnti` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`lt_of_le_of_ne` `div_le_div_right_of_nonpos` `le_of_lt` `ne_of_lt` `mul_div_cancel` `ne_top_of_lt`
`strictMono_div_right_of_pos` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`StrictMono` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`lt_of_le_of_ne` `div_le_div_right_of_nonneg` `le_of_lt` `ne_of_lt` `mul_div_cancel` `ne_bot_of_gt` `ne_of_gt`
`top_div_of_neg_ne_bot` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`DivInvMonoid.toDiv` `instDivInvMonoid` `Top.top` `instTop` `Bot.bot` `instBotEReal`	—	`top_mul_of_neg` `inv_neg_of_neg_ne_bot`
`top_div_of_pos_ne_top` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`DivInvMonoid.toDiv` `instDivInvMonoid` `Top.top` `instTop`	—	`top_mul_of_pos` `inv_pos_of_pos_ne_top`
`zero_div` 📖	mathematical	—	`EReal` `DivInvMonoid.toDiv` `instDivInvMonoid` `instZeroEReal`	—	`MulZeroClass.zero_mul`

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalERealDiv` 📖	CompOp	—
`evalERealInv` 📖	CompOp	—

---

← Back to Index