WithTop

📁 Source: Mathlib/Algebra/Order/Ring/WithTop.lean

Statistics

Metric	Count
Definitions `withTopMap`, `withTopMap`, `instCommMonoidWithZero`, `instCommSemiring`, `instMonoidWithZero`, `instMulZeroClass`, `instMulZeroOneClass`, `instSemigroupWithZero`, `instCommMonoidWithZero`, `instCommSemiring`, `instMonoidWithZero`, `instMulZeroClass`, `instMulZeroOneClass`, `instNonAssocSemiring`, `instNonUnitalNonAssocSemiring`, `instNonUnitalSemiring`, `instSemigroupWithZero`, `instSemiring`	18
Theorems `withTopMap_apply`, `withTopMap_apply`, `bot_lt_mul`, `bot_mul`, `bot_mul'`, `bot_mul_bot`, `coe_mul`, `coe_mul_eq_bind`, `coe_pow`, `instIsOrderedRing`, `instMulPosMono`, `instMulPosReflectLE`, `instMulPosReflectLT`, `instMulPosStrictMono`, `instNoZeroDivisors`, `instPosMulMono`, `instPosMulReflectLE`, `instPosMulReflectLT`, `instPosMulStrictMono`, `mul_bot`, `mul_bot'`, `mul_coe_eq_bind`, `mul_def`, `mul_eq_bot_iff`, `mul_ne_bot`, `unbotD_zero_mul`, `coe_mul`, `coe_mul_eq_bind`, `coe_pow`, `eq_top_of_pow`, `instIsOrderedRing`, `instNoZeroDivisors`, `mul_coe_eq_bind`, `mul_def`, `mul_eq_top_iff`, `mul_left_strictMono`, `mul_lt_mul`, `mul_lt_top`, `mul_ne_top`, `mul_right_strictMono`, `mul_top`, `mul_top'`, `pow_eq_top_iff`, `pow_lt_pow_left`, `pow_lt_top`, `pow_lt_top_iff`, `pow_ne_top`, `pow_ne_top_iff`, `pow_right_strictMono`, `top_mul`, `top_mul'`, `top_mul_top`, `top_pow`, `untopD_zero_mul`	54
Total	72

MonoidWithZeroHom

Definitions

Name	Category	Theorems
`withTopMap` 📖	CompOp	2 math math: `RingHom.withTopMap_apply`, `withTopMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withTopMap_apply` 📖	mathematical	`DFunLike.coe` `MonoidWithZeroHom` `funLike`	`WithTop` `WithTop.instMulZeroOneClass` `withTopMap` `WithTop.map`	—	—

RingHom

Definitions

Name	Category	Theorems
`withTopMap` 📖	CompOp	1 math math: `withTopMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withTopMap_apply` 📖	mathematical	`DFunLike.coe` `RingHom` `instFunLike`	`WithTop` `WithTop.instNonAssocSemiring` `withTopMap` `ZeroHom.toFun` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `WithTop.instMulZeroOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidWithZeroHom.toZeroHom` `MonoidWithZeroHom.withTopMap` `toMonoidWithZeroHom`	—	—

WithBot

Definitions

Name	Category	Theorems
`instCommMonoidWithZero` 📖	CompOp	1 math math: `bot_lt_prod`
`instCommSemiring` 📖	CompOp	6 math math: `Polynomial.degree_pow_le_of_le`, `Polynomial.degree_comp`, `Order.krullDim_le_of_krullDim_preimage_le`, `Polynomial.ringKrullDim_le`, `instIsOrderedRing`, `Order.krullDim_le_of_krullDim_preimage_le'`
`instMonoidWithZero` 📖	CompOp	1 math math: `coe_pow`
`instMulZeroClass` 📖	CompOp	21 math math: `mul_bot'`, `instPosMulStrictMono`, `instMulPosMono`, `mul_coe_eq_bind`, `bot_lt_mul`, `instPosMulReflectLE`, `instMulPosStrictMono`, `instPosMulMono`, `unbotD_zero_mul`, `bot_mul_bot`, `mul_def`, `bot_mul'`, `instNoZeroDivisors`, `mul_eq_bot_iff`, `instMulPosReflectLT`, `mul_bot`, `instMulPosReflectLE`, `bot_mul`, `coe_mul_eq_bind`, `instPosMulReflectLT`, `coe_mul`
`instMulZeroOneClass` 📖	CompOp	—
`instSemigroupWithZero` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_lt_mul` 📖	mathematical	`WithBot` `instLT` `Bot.bot` `bot`	`MulZeroClass.toMul` `instMulZeroClass`	—	`WithTop.mul_lt_top`
`bot_mul` 📖	mathematical	—	`WithBot` `MulZeroClass.toMul` `instMulZeroClass` `Bot.bot` `bot`	—	`bot_mul'`
`bot_mul'` 📖	mathematical	—	`WithBot` `MulZeroClass.toMul` `instMulZeroClass` `Bot.bot` `bot` `zero` `MulZeroClass.toZero` `decidableEq`	—	`if_congr` `coe_eq_zero` `bot_ne_zero`
`bot_mul_bot` 📖	mathematical	—	`WithBot` `MulZeroClass.toMul` `instMulZeroClass` `Bot.bot` `bot`	—	—
`coe_mul` 📖	mathematical	—	`some` `MulZeroClass.toMul` `WithBot` `instMulZeroClass`	—	—
`coe_mul_eq_bind` 📖	mathematical	—	`WithBot` `MulZeroClass.toMul` `instMulZeroClass` `some`	—	`mul_bot`
`coe_pow` 📖	mathematical	—	`some` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `WithBot` `instMonoidWithZero`	—	—
`instIsOrderedRing` 📖	mathematical	—	`IsOrderedRing` `WithBot` `CommSemiring.toSemiring` `instCommSemiring` `instPartialOrder`	—	`isOrderedAddMonoid` `IsOrderedRing.toIsOrderedAddMonoid` `zeroLEOneClass` `IsOrderedRing.toZeroLEOneClass` `instPosMulMono` `IsOrderedRing.toPosMulMono` `instMulPosMono` `IsOrderedRing.toMulPosMono`
`instMulPosMono` 📖	mathematical	—	`MulPosMono` `WithBot` `MulZeroClass.toMul` `instMulZeroClass` `zero` `MulZeroClass.toZero` `instPreorder`	—	`eq_or_ne` `MulZeroClass.mul_zero` `CanLift.prf` `canLift` `LT.lt.not_ge` `bot_lt_coe` `bot_mul` `mul_le_mul_of_nonneg_right`
`instMulPosReflectLE` 📖	mathematical	—	`MulPosReflectLE` `WithBot` `MulZeroClass.toMul` `instMulZeroClass` `zero` `MulZeroClass.toZero` `instPreorder`	—	`CanLift.prf` `canLift` `LT.lt.ne_bot` `bot_le` `coe_mul` `bot_mul` `LT.lt.ne` `LT.lt.not_ge` `bot_lt_coe` `le_of_mul_le_mul_right`
`instMulPosReflectLT` 📖	mathematical	—	`MulPosReflectLT` `WithBot` `MulZeroClass.toMul` `instMulZeroClass` `zero` `MulZeroClass.toZero` `instPreorder`	—	`eq_or_ne` `MulZeroClass.mul_zero` `CanLift.prf` `canLift` `LT.lt.not_ge` `bot_lt_coe` `bot_mul` `LE.le.not_gt` `bot_le` `lt_of_mul_lt_mul_right`
`instMulPosStrictMono` 📖	mathematical	—	`MulPosStrictMono` `WithBot` `MulZeroClass.toMul` `instMulZeroClass` `zero` `MulZeroClass.toZero` `instPreorder`	—	`CanLift.prf` `canLift` `LT.lt.ne_bot` `not_lt_bot` `bot_mul` `LT.lt.ne` `mul_lt_mul_of_pos_right`
`instNoZeroDivisors` 📖	mathematical	—	`NoZeroDivisors` `WithBot` `MulZeroClass.toMul` `instMulZeroClass` `zero` `MulZeroClass.toZero`	—	`WithTop.instNoZeroDivisors`
`instPosMulMono` 📖	mathematical	—	`PosMulMono` `WithBot` `MulZeroClass.toMul` `instMulZeroClass` `zero` `MulZeroClass.toZero` `instPreorder`	—	`eq_or_ne` `MulZeroClass.zero_mul` `CanLift.prf` `canLift` `LT.lt.not_ge` `bot_lt_coe` `mul_bot` `mul_le_mul_of_nonneg_left`
`instPosMulReflectLE` 📖	mathematical	—	`PosMulReflectLE` `WithBot` `MulZeroClass.toMul` `instMulZeroClass` `zero` `MulZeroClass.toZero` `instPreorder`	—	`CanLift.prf` `canLift` `LT.lt.ne_bot` `bot_le` `coe_mul` `mul_bot` `LT.lt.ne` `LT.lt.not_ge` `bot_lt_coe` `le_of_mul_le_mul_left`
`instPosMulReflectLT` 📖	mathematical	—	`PosMulReflectLT` `WithBot` `MulZeroClass.toMul` `instMulZeroClass` `zero` `MulZeroClass.toZero` `instPreorder`	—	`eq_or_ne` `MulZeroClass.zero_mul` `CanLift.prf` `canLift` `LT.lt.not_ge` `bot_lt_coe` `mul_bot` `LE.le.not_gt` `bot_le` `lt_of_mul_lt_mul_left`
`instPosMulStrictMono` 📖	mathematical	—	`PosMulStrictMono` `WithBot` `MulZeroClass.toMul` `instMulZeroClass` `zero` `MulZeroClass.toZero` `instPreorder`	—	`CanLift.prf` `canLift` `LT.lt.ne_bot` `not_lt_bot` `mul_bot` `LT.lt.ne` `mul_lt_mul_of_pos_left`
`mul_bot` 📖	mathematical	—	`WithBot` `MulZeroClass.toMul` `instMulZeroClass` `Bot.bot` `bot`	—	`mul_bot'`
`mul_bot'` 📖	mathematical	—	`WithBot` `MulZeroClass.toMul` `instMulZeroClass` `Bot.bot` `bot` `zero` `MulZeroClass.toZero` `decidableEq`	—	`if_congr` `coe_eq_zero` `bot_ne_zero`
`mul_coe_eq_bind` 📖	mathematical	—	`WithBot` `MulZeroClass.toMul` `instMulZeroClass` `some`	—	`bot_mul`
`mul_def` 📖	mathematical	—	`WithBot` `MulZeroClass.toMul` `instMulZeroClass` `zero` `MulZeroClass.toZero` `decidableEq` `map₂`	—	`mul_bot` `map₂_bot_right` `map₂_coe_right` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero`
`mul_eq_bot_iff` 📖	mathematical	—	`WithBot` `MulZeroClass.toMul` `instMulZeroClass` `Bot.bot` `bot`	—	`mul_def` `map₂_bot_right`
`mul_ne_bot` 📖	—	—	—	—	`WithTop.mul_ne_top`
`unbotD_zero_mul` 📖	mathematical	—	`unbotD` `MulZeroClass.toZero` `WithBot` `MulZeroClass.toMul` `instMulZeroClass`	—	`MulZeroClass.zero_mul` `coe_zero` `unbotD_coe` `MulZeroClass.mul_zero` `bot_mul` `unbotD_bot` `mul_bot` `coe_mul`

WithTop

Definitions

Name	Category	Theorems
`instCommMonoidWithZero` 📖	CompOp	3 math math: `prod_lt_top`, `prod_eq_top`, `prod_eq_top_iff`
`instCommSemiring` 📖	CompOp	—
`instMonoidWithZero` 📖	CompOp	7 math math: `pow_right_strictMono`, `pow_lt_top`, `coe_pow`, `pow_lt_top_iff`, `pow_eq_top_iff`, `pow_lt_pow_left`, `top_pow`
`instMulZeroClass` 📖	CompOp	20 math math: `mul_def`, `top_mul'`, `untop₀_mul`, `top_mul`, `mul_top`, `mul_coe_eq_bind`, `untopD_zero_mul`, `coe_mul_eq_bind`, `ENat.map_natCast_mul`, `mul_top'`, `top_mul_top`, `mul_lt_top`, `meromorphicOrderAt_pow`, `meromorphicOrderAt_zpow`, `mul_left_strictMono`, `coe_mul`, `instNoZeroDivisors`, `mul_right_strictMono`, `MeromorphicAt.meromorphicOrderAt_comp`, `mul_eq_top_iff`
`instMulZeroOneClass` 📖	CompOp	4 math math: `RingHom.ENatMap_apply`, `RingHom.withTopMap_apply`, `MonoidWithZeroHom.withTopMap_apply`, `MonoidWithZeroHom.ENatMap_apply`
`instNonAssocSemiring` 📖	CompOp	2 math math: `RingHom.ENatMap_apply`, `RingHom.withTopMap_apply`
`instNonUnitalNonAssocSemiring` 📖	CompOp	1 math math: `mul_lt_mul`
`instNonUnitalSemiring` 📖	CompOp	—
`instSemigroupWithZero` 📖	CompOp	—
`instSemiring` 📖	CompOp	1 math math: `instIsOrderedRing`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mul` 📖	mathematical	—	`some` `MulZeroClass.toMul` `WithTop` `instMulZeroClass`	—	—
`coe_mul_eq_bind` 📖	mathematical	—	`WithTop` `MulZeroClass.toMul` `instMulZeroClass` `some`	—	`mul_top`
`coe_pow` 📖	mathematical	—	`some` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `WithTop` `instMonoidWithZero`	—	—
`eq_top_of_pow` 📖	—	`WithTop` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `instMonoidWithZero` `Top.top` `top`	—	—	`pow_eq_top_iff`
`instIsOrderedRing` 📖	mathematical	—	`IsOrderedRing` `WithTop` `instSemiring` `CommSemiring.toSemiring` `instPartialOrder`	—	`CanonicallyOrderedAdd.toIsOrderedRing` `canonicallyOrderedAdd`
`instNoZeroDivisors` 📖	mathematical	—	`NoZeroDivisors` `WithTop` `MulZeroClass.toMul` `instMulZeroClass` `zero` `MulZeroClass.toZero`	—	`Option.mem_map₂_iff` `mul_def` `NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero`
`mul_coe_eq_bind` 📖	mathematical	—	`WithTop` `MulZeroClass.toMul` `instMulZeroClass` `some`	—	`top_mul`
`mul_def` 📖	mathematical	—	`WithTop` `MulZeroClass.toMul` `instMulZeroClass` `zero` `MulZeroClass.toZero` `decidableEq` `map₂`	—	`mul_top` `map₂_top_right` `map₂_coe_right` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero`
`mul_eq_top_iff` 📖	mathematical	—	`WithTop` `MulZeroClass.toMul` `instMulZeroClass` `Top.top` `top`	—	`mul_def` `map₂_top_right`
`mul_left_strictMono` 📖	mathematical	`WithTop` `Preorder.toLT` `instPreorder` `zero` `MulZeroClass.toZero`	`StrictMono` `MulZeroClass.toMul` `instMulZeroClass`	—	`CanLift.prf` `canLift` `LT.lt.ne_top` `top_mul` `LT.lt.ne'` `mul_lt_mul_of_pos_right`
`mul_lt_mul` 📖	mathematical	`WithTop` `Preorder.toLT` `instPreorder` `PartialOrder.toPreorder`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `instNonUnitalNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`posMulStrictMono_iff_mulPosStrictMono` `CommMagma.to_isCommutative` `CanLift.prf` `canLift` `LT.lt.ne` `LT.lt.lt_top` `eq_or_ne` `top_mul` `bot_eq_zero` `canonicallyOrderedAdd` `LT.lt.ne'` `LT.lt.bot_lt` `coe_lt_top` `mul_top` `eq_zero_or_pos` `MulZeroClass.mul_zero` `mul_pos` `mul_lt_mul` `PosMulStrictMono.toPosMulMono` `LT.lt.le` `zero_le`
`mul_lt_top` 📖	mathematical	`WithTop` `instLT` `Top.top` `top`	`MulZeroClass.toMul` `instMulZeroClass`	—	`lt_top_iff_ne_top` `mul_ne_top`
`mul_ne_top` 📖	—	—	—	—	—
`mul_right_strictMono` 📖	mathematical	`WithTop` `Preorder.toLT` `instPreorder` `zero` `MulZeroClass.toZero`	`StrictMono` `MulZeroClass.toMul` `instMulZeroClass`	—	`CanLift.prf` `canLift` `LT.lt.ne_top` `mul_top` `LT.lt.ne'` `mul_lt_mul_of_pos_left`
`mul_top` 📖	mathematical	—	`WithTop` `MulZeroClass.toMul` `instMulZeroClass` `Top.top` `top`	—	`mul_top'`
`mul_top'` 📖	mathematical	—	`WithTop` `MulZeroClass.toMul` `instMulZeroClass` `Top.top` `top` `zero` `MulZeroClass.toZero` `decidableEq`	—	`if_congr` `coe_eq_zero` `top_ne_zero`
`pow_eq_top_iff` 📖	mathematical	—	`WithTop` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `instMonoidWithZero` `Top.top` `top`	—	`pow_zero` `top_pow`
`pow_lt_pow_left` 📖	mathematical	`WithTop` `Preorder.toLT` `instPreorder` `PartialOrder.toPreorder`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `instMonoidWithZero` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	—	`pow_right_strictMono`
`pow_lt_top` 📖	mathematical	`WithTop` `Preorder.toLT` `instPreorder` `Top.top` `top`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `instMonoidWithZero`	—	`pow_lt_top_iff`
`pow_lt_top_iff` 📖	mathematical	—	`WithTop` `Preorder.toLT` `instPreorder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `instMonoidWithZero` `Top.top` `top`	—	—
`pow_ne_top` 📖	—	—	—	—	`pow_ne_top_iff`
`pow_ne_top_iff` 📖	—	—	—	—	—
`pow_right_strictMono` 📖	mathematical	—	`StrictMono` `WithTop` `instPreorder` `PartialOrder.toPreorder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `instMonoidWithZero` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	—	`pow_one` `strictMono_id` `pow_succ` `mul_lt_mul`
`top_mul` 📖	mathematical	—	`WithTop` `MulZeroClass.toMul` `instMulZeroClass` `Top.top` `top`	—	`top_mul'`
`top_mul'` 📖	mathematical	—	`WithTop` `MulZeroClass.toMul` `instMulZeroClass` `Top.top` `top` `zero` `MulZeroClass.toZero` `decidableEq`	—	`if_congr` `coe_eq_zero` `top_ne_zero`
`top_mul_top` 📖	mathematical	—	`WithTop` `MulZeroClass.toMul` `instMulZeroClass` `Top.top` `top`	—	—
`top_pow` 📖	mathematical	—	`WithTop` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `instMonoidWithZero` `Top.top` `top`	—	—
`untopD_zero_mul` 📖	mathematical	—	`untopD` `MulZeroClass.toZero` `WithTop` `MulZeroClass.toMul` `instMulZeroClass`	—	`MulZeroClass.zero_mul` `coe_zero` `untopD_coe` `MulZeroClass.mul_zero` `top_mul` `untopD_top` `mul_top` `coe_mul`

---

← Back to Index