| Metric | Count |
|---|
DefinitionsinstPow, instPow', instSMul, instSMul', instVAdd, instVAdd', instPow, instPow', instSMul, instSMul', instVAdd, instVAdd', instAddCancelCommMonoid, instAddCommMonoid, instAddGroup, instCancelCommMonoid, instCommMonoid, instGroup, instPow, instPow', instSMul, instSMul', instVAdd, instVAdd', instAddCancelCommMonoidColex, instAddCancelCommMonoidLex, instAddCancelMonoidColex, instAddCancelMonoidLex, instAddCancelMonoidOrderDual, instAddColex, instAddCommGroupColex, instAddCommGroupLex, instAddCommGroupOrderDual, instAddCommMonoidColex, instAddCommMonoidLex, instAddCommSemigroupColex, instAddCommSemigroupLex, instAddCommSemigroupOrderDual, instAddGroupColex, instAddGroupLex, instAddLeftCancelMonoidColex, instAddLeftCancelMonoidLex, instAddLeftCancelMonoidOrderDual, instAddLeftCancelSemigroupColex, instAddLeftCancelSemigroupLex, instAddLeftCancelSemigroupOrderDual, instAddLex, instAddMonoidColex, instAddMonoidLex, instAddMonoidOrderDual, instAddOrderDual, instAddRightCancelMonoidColex, instAddRightCancelMonoidLex, instAddRightCancelMonoidOrderDual, instAddRightCancelSemigroupColex, instAddRightCancelSemigroupLex, instAddRightCancelSemigroupOrderDual, instAddSemigroupColex, instAddSemigroupLex, instAddSemigroupOrderDual, instAddZeroClassColex, instAddZeroClassLex, instAddZeroClassOrderDual, instCancelCommMonoidColex, instCancelCommMonoidLex, instCancelMonoidColex, instCancelMonoidLex, instCancelMonoidOrderDual, instCommGroupColex, instCommGroupLex, instCommGroupOrderDual, instCommMonoidColex, instCommMonoidLex, instCommSemigroupColex, instCommSemigroupLex, instCommSemigroupOrderDual, instDivColex, instDivInvMonoidColex, instDivInvMonoidLex, instDivInvMonoidOrderDual, instDivLex, instDivOrderDual, instDivisionAddCommMonoidColex, instDivisionAddCommMonoidLex, instDivisionAddCommMonoidOrderDual, instDivisionCommMonoidColex, instDivisionCommMonoidLex, instDivisionCommMonoidOrderDual, instDivisionMonoidColex, instDivisionMonoidLex, instDivisionMonoidOrderDual, instGroupColex, instGroupLex, instInvColex, instInvLex, instInvOrderDual, instInvolutiveInvColex, instInvolutiveInvLex, instInvolutiveInvOrderDual, instInvolutiveNegColex, instInvolutiveNegLex, instInvolutiveNegOrderDual, instLeftCancelMonoidColex, instLeftCancelMonoidLex, instLeftCancelMonoidOrderDual, instLeftCancelSemigroupColex, instLeftCancelSemigroupLex, instLeftCancelSemigroupOrderDual, instMonoidColex, instMonoidLex, instMonoidOrderDual, instMulColex, instMulLex, instMulOneClassColex, instMulOneClassLex, instMulOneClassOrderDual, instMulOrderDual, instNegColex, instNegLex, instNegOrderDual, instOneColex, instOneLex, instOneOrderDual, instRightCancelMonoidColex, instRightCancelMonoidLex, instRightCancelMonoidOrderDual, instRightCancelSemigroupColex, instRightCancelSemigroupLex, instRightCancelSemigroupOrderDual, instSemigroupColex, instSemigroupLex, instSemigroupOrderDual, instSubColex, instSubLex, instSubNegAddMonoidColex, instSubNegAddMonoidLex, instSubNegAddMonoidOrderDual, instSubOrderDual, instSubtractionMonoidColex, instSubtractionMonoidLex, instSubtractionMonoidOrderDual, instZeroColex, instZeroLex, instZeroOrderDual | 144 |
TheoremsinstIsCancelAddColex, instIsCancelAddLex, instIsCancelAddOrderDual, instIsCancelMulColex, instIsCancelMulLex, instIsCancelMulOrderDual, instIsLeftCancelAddColex, instIsLeftCancelAddLex, instIsLeftCancelAddOrderDual, instIsLeftCancelMulColex, instIsLeftCancelMulLex, instIsLeftCancelMulOrderDual, instIsRightCancelAddColex, instIsRightCancelAddLex, instIsRightCancelAddOrderDual, instIsRightCancelMulColex, instIsRightCancelMulLex, instIsRightCancelMulOrderDual, isAddLeftRegular_ofColex, isAddLeftRegular_ofDual, isAddLeftRegular_ofLex, isAddLeftRegular_toColex, isAddLeftRegular_toDual, isAddLeftRegular_toLex, isAddRegular_ofColex, isAddRegular_ofDual, isAddRegular_ofLex, isAddRegular_toColex, isAddRegular_toDual, isAddRegular_toLex, isAddRightRegular_ofColex, isAddRightRegular_ofDual, isAddRightRegular_ofLex, isAddRightRegular_toColex, isAddRightRegular_toDual, isAddRightRegular_toLex, isLeftRegular_ofColex, isLeftRegular_ofDual, isLeftRegular_ofLex, isLeftRegular_toColex, isLeftRegular_toDual, isLeftRegular_toLex, isRegular_ofColex, isRegular_ofDual, isRegular_ofLex, isRegular_toColex, isRegular_toDual, isRegular_toLex, isRightRegular_ofColex, isRightRegular_ofDual, isRightRegular_ofLex, isRightRegular_toColex, isRightRegular_toDual, isRightRegular_toLex, ofColex_add, ofColex_div, ofColex_eq_one, ofColex_eq_zero, ofColex_inv, ofColex_mul, ofColex_neg, ofColex_one, ofColex_pow, ofColex_smul, ofColex_smul', ofColex_sub, ofColex_vadd, ofColex_vadd', ofColex_zero, ofDual_add, ofDual_div, ofDual_eq_one, ofDual_eq_zero, ofDual_inv, ofDual_mul, ofDual_neg, ofDual_one, ofDual_pow, ofDual_smul, ofDual_smul', ofDual_sub, ofDual_vadd, ofDual_vadd', ofDual_zero, ofLex_add, ofLex_div, ofLex_eq_one, ofLex_eq_zero, ofLex_inv, ofLex_mul, ofLex_neg, ofLex_one, ofLex_pow, ofLex_smul, ofLex_smul', ofLex_sub, ofLex_vadd, ofLex_vadd', ofLex_zero, pow_ofColex, pow_ofDual, pow_ofLex, pow_toColex, pow_toDual, pow_toLex, toColex_add, toColex_div, toColex_eq_one, toColex_eq_zero, toColex_inv, toColex_mul, toColex_neg, toColex_one, toColex_pow, toColex_smul, toColex_smul', toColex_sub, toColex_vadd, toColex_vadd', toColex_zero, toDual_add, toDual_div, toDual_eq_one, toDual_eq_zero, toDual_inv, toDual_mul, toDual_neg, toDual_one, toDual_pow, toDual_smul, toDual_smul', toDual_sub, toDual_vadd, toDual_vadd', toDual_zero, toLex_add, toLex_div, toLex_eq_one, toLex_eq_zero, toLex_inv, toLex_mul, toLex_neg, toLex_one, toLex_pow, toLex_smul, toLex_smul', toLex_sub, toLex_vadd, toLex_vadd', toLex_zero | 150 |
| Total | 294 |
| Name | Category | Theorems |
|---|
instAddCancelCommMonoidColex 📖 | CompOp | — |
instAddCancelCommMonoidLex 📖 | CompOp | — |
instAddCancelMonoidColex 📖 | CompOp | — |
instAddCancelMonoidLex 📖 | CompOp | — |
instAddCancelMonoidOrderDual 📖 | CompOp | — |
instAddColex 📖 | CompOp | 19 mathmath: Finsupp.Colex.addLeftStrictMono, instIsRightCancelAddColex, toColex_add, ofColex_add, DFinsupp.Colex.addRightMono, isAddRightRegular_toColex, isAddLeftRegular_ofColex, Finsupp.Colex.addRightMono, Finsupp.Colex.addRightStrictMono, isAddRegular_ofColex, isAddRightRegular_ofColex, instIsCancelAddColex, Finsupp.Colex.addLeftMono, isAddRegular_toColex, DFinsupp.Colex.addLeftStrictMono, DFinsupp.Colex.addRightStrictMono, isAddLeftRegular_toColex, DFinsupp.Colex.addLeftMono, instIsLeftCancelAddColex
|
instAddCommGroupColex 📖 | CompOp | — |
instAddCommGroupLex 📖 | CompOp | 23 mathmath: HahnEmbedding.IsPartial.baseEmbedding_le, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, HahnEmbedding.Partial.archimedeanClassMk_eq_iff, HahnEmbedding.Seed.baseEmbedding_strictMono, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, HahnEmbedding.Partial.orderTop_eq_iff, HahnEmbedding.IsPartial.strictMono, HahnEmbedding.IsPartial.truncLT_mem_range, HahnSeries.archimedeanClassMk_eq_archimedeanClassMk_iff, HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_snd, HahnSeries.archimedeanClassOrderIsoWithTop_apply, HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff_of_orderTop_ofLex, HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, HahnEmbedding.Partial.mem_domain, HahnEmbedding.Seed.mem_domain_baseEmbedding, HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff, HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_fst, HahnSeries.finiteArchimedeanClassOrderIso_apply, HahnEmbedding.Partial.exists_domain_eq_top, HahnEmbedding.Partial.exists_isMax, HahnEmbedding.Seed.domain_baseEmbedding, HahnEmbedding.Partial.toOrderAddMonoidHom_injective
|
instAddCommGroupOrderDual 📖 | CompOp | — |
instAddCommMonoidColex 📖 | CompOp | 3 mathmath: DFinsupp.Colex.isOrderedCancelAddMonoid, Finsupp.Colex.isOrderedCancelAddMonoid, DFinsupp.Colex.isOrderedAddMonoid
|
instAddCommMonoidLex 📖 | CompOp | 14 mathmath: instIsOrderedCancelAddMonoidLexFinsupp, DFinsupp.Lex.isOrderedCancelAddMonoid, Prod.Lex.isOrderedAddMonoid, DFinsupp.Lex.isOrderedAddMonoid, symm_toLexLinearEquiv, coe_toLexLinearEquiv, Pi.Lex.isOrderedAddCancelMonoid, hahnEmbedding_isOrderedModule_rat, Finsupp.Lex.isOrderedCancelAddMonoid, HahnSeries.instIsOrderedAddMonoidLex, coe_ofLexLinearEquiv, hahnEmbedding_isOrderedModule, symm_ofLexLinearEquiv, Prod.Lex.isOrderedAddCancelMonoid
|
instAddCommSemigroupColex 📖 | CompOp | — |
instAddCommSemigroupLex 📖 | CompOp | — |
instAddCommSemigroupOrderDual 📖 | CompOp | — |
instAddGroupColex 📖 | CompOp | — |
instAddGroupLex 📖 | CompOp | 5 mathmath: HahnSeries.support_abs, HahnSeries.abs_lt_abs_of_orderTop_ofLex, HahnSeries.order_abs, HahnSeries.orderTop_abs, HahnSeries.leadingCoeff_abs
|
instAddLeftCancelMonoidColex 📖 | CompOp | — |
instAddLeftCancelMonoidLex 📖 | CompOp | — |
instAddLeftCancelMonoidOrderDual 📖 | CompOp | — |
instAddLeftCancelSemigroupColex 📖 | CompOp | — |
instAddLeftCancelSemigroupLex 📖 | CompOp | — |
instAddLeftCancelSemigroupOrderDual 📖 | CompOp | — |
instAddLex 📖 | CompOp | 32 mathmath: instIsCancelAddLex, ofLex_add, Finsupp.Lex.addLeftMono, OrderAddMonoidHom.addCommute_inlₗ_inrₗ, symm_ofLexAddEquiv, MvPowerSeries.lexOrder_mul, toLex_add, isAddLeftRegular_toLex, symm_toLexAddEquiv, isAddRightRegular_toLex, DFinsupp.Lex.addLeftStrictMono, DFinsupp.Lex.addRightStrictMono, isAddRegular_toLex, DFinsupp.Lex.addRightMono, isAddRightRegular_ofLex, Finsupp.Lex.addRightStrictMono, coe_ofLexAddEquiv, OrderAddMonoidHom.inlₗ_add_inrₗ_eq_toLex, Finsupp.Lex.addLeftStrictMono, instIsLeftCancelAddLex, DFinsupp.Lex.addLeftMono, isAddRegular_ofLex, toEquiv_toLexAddEquiv, isAddLeftRegular_ofLex, Finsupp.Lex.addRightMono, instIsRightCancelAddLex, MvPowerSeries.le_lexOrder_mul, instRightDistribClassLex, coe_toLexAddEquiv, instLeftDistribClassLex, toEquiv_ofLexAddEquiv, MvPowerSeries.lexOrder_mul_ge
|
instAddMonoidColex 📖 | CompOp | — |
instAddMonoidLex 📖 | CompOp | — |
instAddMonoidOrderDual 📖 | CompOp | 1 mathmath: instLipschitzAddOrderDual
|
instAddOrderDual 📖 | CompOp | 22 mathmath: instIsRightCancelAddOrderDual, OrderDual.addRightMono, isAddLeftRegular_ofDual, instContinuousAddOrderDual, isAddRightRegular_ofDual, OrderDual.addLeftMono, instLeftDistribClassOrderDual, isAddRightRegular_toDual, OrderDual.addRightReflectLT, isAddLeftRegular_toDual, OrderDual.addRightStrictMono, isAddRegular_ofDual, instRightDistribClassOrderDual, instIsCancelAddOrderDual, OrderDual.addRightReflectLE, OrderDual.addLeftReflectLT, instIsLeftCancelAddOrderDual, OrderDual.addLeftReflectLE, ofDual_add, isAddRegular_toDual, toDual_add, OrderDual.addLeftStrictMono
|
instAddRightCancelMonoidColex 📖 | CompOp | — |
instAddRightCancelMonoidLex 📖 | CompOp | — |
instAddRightCancelMonoidOrderDual 📖 | CompOp | — |
instAddRightCancelSemigroupColex 📖 | CompOp | — |
instAddRightCancelSemigroupLex 📖 | CompOp | — |
instAddRightCancelSemigroupOrderDual 📖 | CompOp | — |
instAddSemigroupColex 📖 | CompOp | — |
instAddSemigroupLex 📖 | CompOp | — |
instAddSemigroupOrderDual 📖 | CompOp | — |
instAddZeroClassColex 📖 | CompOp | — |
instAddZeroClassLex 📖 | CompOp | 11 mathmath: OrderAddMonoidHom.addCommute_inlₗ_inrₗ, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, OrderAddMonoidHom.fstₗ_comp_inlₗ, HahnSeries.embDomainOrderAddMonoidHom_injective, OrderAddMonoidHom.inlₗ_apply, OrderAddMonoidHom.inlₗ_add_inrₗ_eq_toLex, HahnSeries.embDomainOrderAddMonoidHom_apply, OrderAddMonoidHom.fstₗ_apply, OrderAddMonoidHom.inrₗ_apply, hahnEmbedding_isOrderedAddMonoid, HahnEmbedding.Partial.toOrderAddMonoidHom_injective
|
instAddZeroClassOrderDual 📖 | CompOp | — |
instCancelCommMonoidColex 📖 | CompOp | — |
instCancelCommMonoidLex 📖 | CompOp | — |
instCancelMonoidColex 📖 | CompOp | — |
instCancelMonoidLex 📖 | CompOp | — |
instCancelMonoidOrderDual 📖 | CompOp | — |
instCommGroupColex 📖 | CompOp | — |
instCommGroupLex 📖 | CompOp | — |
instCommGroupOrderDual 📖 | CompOp | — |
instCommMonoidColex 📖 | CompOp | — |
instCommMonoidLex 📖 | CompOp | 3 mathmath: Prod.Lex.isOrderedCancelMonoid, Pi.Lex.isOrderedCancelMonoid, Prod.Lex.isOrderedMonoid
|
instCommSemigroupColex 📖 | CompOp | — |
instCommSemigroupLex 📖 | CompOp | — |
instCommSemigroupOrderDual 📖 | CompOp | — |
instDivColex 📖 | CompOp | 2 mathmath: ofColex_div, toColex_div
|
instDivInvMonoidColex 📖 | CompOp | — |
instDivInvMonoidLex 📖 | CompOp | — |
instDivInvMonoidOrderDual 📖 | CompOp | — |
instDivLex 📖 | CompOp | 2 mathmath: toLex_div, ofLex_div
|
instDivOrderDual 📖 | CompOp | 2 mathmath: toDual_div, ofDual_div
|
instDivisionAddCommMonoidColex 📖 | CompOp | — |
instDivisionAddCommMonoidLex 📖 | CompOp | — |
instDivisionAddCommMonoidOrderDual 📖 | CompOp | — |
instDivisionCommMonoidColex 📖 | CompOp | — |
instDivisionCommMonoidLex 📖 | CompOp | — |
instDivisionCommMonoidOrderDual 📖 | CompOp | — |
instDivisionMonoidColex 📖 | CompOp | — |
instDivisionMonoidLex 📖 | CompOp | — |
instDivisionMonoidOrderDual 📖 | CompOp | — |
instGroupColex 📖 | CompOp | — |
instGroupLex 📖 | CompOp | — |
instInvColex 📖 | CompOp | 2 mathmath: toColex_inv, ofColex_inv
|
instInvLex 📖 | CompOp | 2 mathmath: toLex_inv, ofLex_inv
|
instInvOrderDual 📖 | CompOp | 4 mathmath: toDual_inv, OrderDual.instContinuousInv, OrderIso.invENNReal_apply, ofDual_inv
|
instInvolutiveInvColex 📖 | CompOp | — |
instInvolutiveInvLex 📖 | CompOp | — |
instInvolutiveInvOrderDual 📖 | CompOp | — |
instInvolutiveNegColex 📖 | CompOp | — |
instInvolutiveNegLex 📖 | CompOp | — |
instInvolutiveNegOrderDual 📖 | CompOp | — |
instLeftCancelMonoidColex 📖 | CompOp | — |
instLeftCancelMonoidLex 📖 | CompOp | — |
instLeftCancelMonoidOrderDual 📖 | CompOp | — |
instLeftCancelSemigroupColex 📖 | CompOp | — |
instLeftCancelSemigroupLex 📖 | CompOp | — |
instLeftCancelSemigroupOrderDual 📖 | CompOp | — |
instMonoidColex 📖 | CompOp | — |
instMonoidLex 📖 | CompOp | — |
instMonoidOrderDual 📖 | CompOp | 1 mathmath: instLipschitzMulOrderDual
|
instMulColex 📖 | CompOp | 11 mathmath: isLeftRegular_ofColex, ofColex_mul, isRightRegular_toColex, instIsCancelMulColex, instIsRightCancelMulColex, toColex_mul, isRightRegular_ofColex, instIsLeftCancelMulColex, isRegular_toColex, isRegular_ofColex, isLeftRegular_toColex
|
instMulLex 📖 | CompOp | 26 mathmath: toLex_mul, isLeftRegular_toLex, LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex, toEquiv_toLexMulEquiv, isRightRegular_ofLex, isRegular_toLex, instIsCancelMulLex, coe_ofLexMulEquiv, OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex, instIsCancelMulZeroLex, instIsRightCancelMulLex, instIsLeftCancelMulLex, isRightRegular_toLex, OrderMonoidHom.commute_inlₗ_inrₗ, symm_ofLexMulEquiv, instIsLeftCancelMulZeroLex, toEquiv_ofLexMulEquiv, instIsRightCancelMulZeroLex, instNoZeroDivisorsLex, coe_toLexMulEquiv, ofLex_mul, symm_toLexMulEquiv, isLeftRegular_ofLex, isRegular_ofLex, instRightDistribClassLex, instLeftDistribClassLex
|
instMulOneClassColex 📖 | CompOp | — |
instMulOneClassLex 📖 | CompOp | 13 mathmath: LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex, OrderMonoidHom.inrₗ_apply, OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex, LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ, OrderMonoidHom.inlₗ_apply, OrderMonoidHom.fstₗ_apply, LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ, OrderMonoidHom.commute_inlₗ_inrₗ, LinearOrderedCommGroupWithZero.fst_comp_inl, LinearOrderedCommGroupWithZero.fst_apply, OrderMonoidHom.fstₗ_comp_inlₗ, LinearOrderedCommGroupWithZero.inl_apply, LinearOrderedCommGroupWithZero.inr_apply
|
instMulOneClassOrderDual 📖 | CompOp | — |
instMulOrderDual 📖 | CompOp | 26 mathmath: OrderDual.mulLeftReflectLT, instIsRightCancelMulOrderDual, instIsLeftCancelMulZeroOrderDual, instNoZeroDivisorsOrderDual, instIsCancelMulOrderDual, OrderDual.mulLeftReflectLE, instIsCancelMulZeroOrderDual, toDual_mul, OrderDual.mulLeftStrictMono, instIsRightCancelMulZeroOrderDual, isRightRegular_toDual, instIsLeftCancelMulOrderDual, instLeftDistribClassOrderDual, OrderDual.mulLeftMono, OrderDual.mulRightStrictMono, isLeftRegular_ofDual, instRightDistribClassOrderDual, isRightRegular_ofDual, isLeftRegular_toDual, isRegular_toDual, OrderDual.mulRightMono, instContinuousMulOrderDual, isRegular_ofDual, ofDual_mul, OrderDual.mulRightReflectLE, OrderDual.mulRightReflectLT
|
instNegColex 📖 | CompOp | 2 mathmath: toColex_neg, ofColex_neg
|
instNegLex 📖 | CompOp | 2 mathmath: ofLex_neg, toLex_neg
|
instNegOrderDual 📖 | CompOp | 3 mathmath: OrderDual.instContinuousNeg, ofDual_neg, toDual_neg
|
instOneColex 📖 | CompOp | 4 mathmath: ofColex_one, toColex_one, ofColex_eq_one, toColex_eq_one
|
instOneLex 📖 | CompOp | 4 mathmath: toLex_eq_one, ofLex_eq_one, ofLex_one, toLex_one
|
instOneOrderDual 📖 | CompOp | 4 mathmath: ofDual_eq_one, ofDual_one, toDual_eq_one, toDual_one
|
instRightCancelMonoidColex 📖 | CompOp | — |
instRightCancelMonoidLex 📖 | CompOp | — |
instRightCancelMonoidOrderDual 📖 | CompOp | — |
instRightCancelSemigroupColex 📖 | CompOp | — |
instRightCancelSemigroupLex 📖 | CompOp | — |
instRightCancelSemigroupOrderDual 📖 | CompOp | — |
instSemigroupColex 📖 | CompOp | — |
instSemigroupLex 📖 | CompOp | — |
instSemigroupOrderDual 📖 | CompOp | — |
instSubColex 📖 | CompOp | 2 mathmath: toColex_sub, ofColex_sub
|
instSubLex 📖 | CompOp | 2 mathmath: toLex_sub, ofLex_sub
|
instSubNegAddMonoidColex 📖 | CompOp | — |
instSubNegAddMonoidLex 📖 | CompOp | — |
instSubNegAddMonoidOrderDual 📖 | CompOp | — |
instSubOrderDual 📖 | CompOp | 2 mathmath: toDual_sub, ofDual_sub
|
instSubtractionMonoidColex 📖 | CompOp | — |
instSubtractionMonoidLex 📖 | CompOp | — |
instSubtractionMonoidOrderDual 📖 | CompOp | — |
instZeroColex 📖 | CompOp | 4 mathmath: toColex_eq_zero, ofColex_eq_zero, toColex_zero, ofColex_zero
|
instZeroLex 📖 | CompOp | 15 mathmath: HahnEmbedding.Seed.baseEmbedding_pos, instIsCancelMulZeroLex, HahnSeries.leadingCoeff_pos_iff, toLex_zero, MvPolynomial.supDegree_toLex_C, instIsLeftCancelMulZeroLex, HahnSeries.leadingCoeff_nonneg_iff, instIsRightCancelMulZeroLex, instNoZeroDivisorsLex, HahnEmbedding.Partial.eval_zero, toLex_eq_zero, HahnSeries.leadingCoeff_neg_iff, ofLex_eq_zero, HahnSeries.leadingCoeff_nonpos_iff, ofLex_zero
|
instZeroOrderDual 📖 | CompOp | 14 mathmath: OrderDual.instIsStrictOrderedModule, toDual_zero, toDual_eq_zero, instIsLeftCancelMulZeroOrderDual, OrderDual.instSMulPosStrictMono, instNoZeroDivisorsOrderDual, instIsCancelMulZeroOrderDual, OrderDual.instSMulPosReflectLE, instIsRightCancelMulZeroOrderDual, OrderDual.instSMulPosMono, OrderDual.instSMulPosReflectLT, OrderDual.instIsOrderedModule, ofDual_zero, ofDual_eq_zero
|