| Metric | Count |
|---|
DefinitionsinstPow, instPow', instSMul, instSMul', instVAdd, instVAdd', instPow, instPow', instSMul, instSMul', instVAdd, instVAdd', instAdd, instAddCancelCommMonoid, instAddCancelMonoid, instAddCommGroup, instAddCommMonoid, instAddCommSemigroup, instAddGroup, instAddLeftCancelMonoid, instAddLeftCancelSemigroup, instAddMonoid, instAddRightCancelMonoid, instAddRightCancelSemigroup, instAddSemigroup, instAddZeroClass, instCancelCommMonoid, instCancelMonoid, instCommGroup, instCommMonoid, instCommSemigroup, instDiv, instDivInvMonoid, instDivisionAddCommMonoid, instDivisionCommMonoid, instDivisionMonoid, instGroup, instInv, instInvolutiveInv, instInvolutiveNeg, instLeftCancelMonoid, instLeftCancelSemigroup, instMonoid, instMul, instMulOneClass, instNeg, instOne, instPow, instPow_1, instRightCancelMonoid, instRightCancelSemigroup, instSMul, instSMul', instSemigroup, instSub, instSubNegAddMonoid, instSubtractionMonoid, instVAdd, instVAdd', instZero, instAddCancelCommMonoidColex, instAddCancelCommMonoidLex, instAddCancelMonoidColex, instAddCancelMonoidLex, instAddColex, instAddCommGroupColex, instAddCommGroupLex, instAddCommMonoidColex, instAddCommMonoidLex, instAddCommSemigroupColex, instAddCommSemigroupLex, instAddGroupColex, instAddGroupLex, instAddLeftCancelMonoidColex, instAddLeftCancelMonoidLex, instAddLeftCancelSemigroupColex, instAddLeftCancelSemigroupLex, instAddLex, instAddMonoidColex, instAddMonoidLex, instAddRightCancelMonoidColex, instAddRightCancelMonoidLex, instAddRightCancelSemigroupColex, instAddRightCancelSemigroupLex, instAddSemigroupColex, instAddSemigroupLex, instAddZeroClassColex, instAddZeroClassLex, instCancelCommMonoidColex, instCancelCommMonoidLex, instCancelMonoidColex, instCancelMonoidLex, instCommGroupColex, instCommGroupLex, instCommMonoidColex, instCommMonoidLex, instCommSemigroupColex, instCommSemigroupLex, instDivColex, instDivInvMonoidColex, instDivInvMonoidLex, instDivLex, instDivisionAddCommMonoidColex, instDivisionAddCommMonoidLex, instDivisionCommMonoidColex, instDivisionCommMonoidLex, instDivisionMonoidColex, instDivisionMonoidLex, instGroupColex, instGroupLex, instInvColex, instInvLex, instInvolutiveInvColex, instInvolutiveInvLex, instInvolutiveNegColex, instInvolutiveNegLex, instLeftCancelMonoidColex, instLeftCancelMonoidLex, instLeftCancelSemigroupColex, instLeftCancelSemigroupLex, instMonoidColex, instMonoidLex, instMulColex, instMulLex, instMulOneClassColex, instMulOneClassLex, instNegColex, instNegLex, instOneColex, instOneLex, instRightCancelMonoidColex, instRightCancelMonoidLex, instRightCancelSemigroupColex, instRightCancelSemigroupLex, instSemigroupColex, instSemigroupLex, instSubColex, instSubLex, instSubNegAddMonoidColex, instSubNegAddMonoidLex, instSubtractionMonoidColex, instSubtractionMonoidLex, instZeroColex, instZeroLex | 144 |
TheoremsinstIsCancelAdd, instIsCancelMul, instIsLeftCancelAdd, instIsLeftCancelMul, instIsRightCancelAdd, instIsRightCancelMul, instIsCancelAddColex, instIsCancelAddLex, instIsCancelMulColex, instIsCancelMulLex, instIsLeftCancelAddColex, instIsLeftCancelAddLex, instIsLeftCancelMulColex, instIsLeftCancelMulLex, instIsRightCancelAddColex, instIsRightCancelAddLex, instIsRightCancelMulColex, instIsRightCancelMulLex, 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 |
|---|
instAdd 📖 | CompOp | 23 mathmath: instIsRightCancelAdd, instIsLeftCancelAdd, addRightMono, isAddLeftRegular_ofDual, instContinuousAddOrderDual, isAddRightRegular_ofDual, addLeftMono, instIsCancelAdd, isAddRightRegular_toDual, instLeftDistribClass, addRightReflectLT, isAddLeftRegular_toDual, addRightStrictMono, isAddRegular_ofDual, instSeparatelyContinuousAddOrderDual, addRightReflectLE, addLeftReflectLT, addLeftReflectLE, ofDual_add, isAddRegular_toDual, toDual_add, instRightDistribClass, addLeftStrictMono
|
instAddCancelCommMonoid 📖 | CompOp | — |
instAddCancelMonoid 📖 | CompOp | — |
instAddCommGroup 📖 | CompOp | — |
instAddCommMonoid 📖 | CompOp | 7 mathmath: instAddArchimedean, ConvexOn.dual, isOrderedAddCancelMonoid, StrictConvexOn.dual, StrictConcaveOn.dual, isOrderedAddMonoid, ConcaveOn.dual
|
instAddCommSemigroup 📖 | CompOp | — |
instAddGroup 📖 | CompOp | 1 mathmath: instIsTopologicalAddGroup
|
instAddLeftCancelMonoid 📖 | CompOp | — |
instAddLeftCancelSemigroup 📖 | CompOp | — |
instAddMonoid 📖 | CompOp | 1 mathmath: instLipschitzAddOrderDual
|
instAddRightCancelMonoid 📖 | CompOp | — |
instAddRightCancelSemigroup 📖 | CompOp | — |
instAddSemigroup 📖 | CompOp | — |
instAddZeroClass 📖 | CompOp | — |
instCancelCommMonoid 📖 | CompOp | — |
instCancelMonoid 📖 | CompOp | — |
instCommGroup 📖 | CompOp | — |
instCommMonoid 📖 | CompOp | 3 mathmath: instMulArchimedean, isOrderedCancelMonoid, isOrderedMonoid
|
instCommSemigroup 📖 | CompOp | — |
instDiv 📖 | CompOp | 2 mathmath: toDual_div, ofDual_div
|
instDivInvMonoid 📖 | CompOp | — |
instDivisionAddCommMonoid 📖 | CompOp | — |
instDivisionCommMonoid 📖 | CompOp | — |
instDivisionMonoid 📖 | CompOp | — |
instGroup 📖 | CompOp | 1 mathmath: instIsTopologicalGroup
|
instInv 📖 | CompOp | 4 mathmath: toDual_inv, instContinuousInv, OrderIso.invENNReal_apply, ofDual_inv
|
instInvolutiveInv 📖 | CompOp | — |
instInvolutiveNeg 📖 | CompOp | — |
instLeftCancelMonoid 📖 | CompOp | — |
instLeftCancelSemigroup 📖 | CompOp | — |
instMonoid 📖 | CompOp | 1 mathmath: instLipschitzMulOrderDual
|
instMul 📖 | CompOp | 27 mathmath: instIsRightCancelMulZero, mulLeftReflectLT, instSeparatelyContinuousMulOrderDual, instIsRightCancelMul, mulLeftReflectLE, toDual_mul, mulLeftStrictMono, instIsCancelMul, isRightRegular_toDual, mulLeftMono, mulRightStrictMono, instLeftDistribClass, isLeftRegular_ofDual, isRightRegular_ofDual, instIsCancelMulZero, instIsLeftCancelMul, isLeftRegular_toDual, instNoZeroDivisors, isRegular_toDual, mulRightMono, instContinuousMulOrderDual, isRegular_ofDual, ofDual_mul, instRightDistribClass, mulRightReflectLE, mulRightReflectLT, instIsLeftCancelMulZero
|
instMulOneClass 📖 | CompOp | — |
instNeg 📖 | CompOp | 3 mathmath: instContinuousNeg, ofDual_neg, toDual_neg
|
instOne 📖 | CompOp | 4 mathmath: ofDual_eq_one, ofDual_one, toDual_eq_one, toDual_one
|
instPow 📖 | CompOp | 2 mathmath: toDual_pow, ofDual_pow
|
instPow_1 📖 | CompOp | 2 mathmath: pow_ofDual, pow_toDual
|
instRightCancelMonoid 📖 | CompOp | — |
instRightCancelSemigroup 📖 | CompOp | — |
instSMul 📖 | CompOp | 22 mathmath: instPosSMulMono, instIsScalarTower_1, instIsStrictOrderedModule, ofDual_smul, OrderIso.smulRightDual_apply, instPosSMulReflectLE, instSMulPosStrictMono, instPosSMulReflectLT, instIsScalarTower_2, instSMulCommClass_2, instSMulPosReflectLE, ConvexOn.dual, instPosSMulStrictMono, instSMulPosMono, instSMulPosReflectLT, instIsOrderedModule, StrictConvexOn.dual, StrictConcaveOn.dual, toDual_smul, instContinuousSMul_right, instContinuousConstSMulOrderDual, ConcaveOn.dual
|
instSMul' 📖 | CompOp | 8 mathmath: continuousConstSMul', instIsScalarTower_1, toDual_smul', instSMulCommClass_1, instSMulCommClass, instIsScalarTower, instContinuousSMul_left, ofDual_smul'
|
instSemigroup 📖 | CompOp | — |
instSub 📖 | CompOp | 2 mathmath: toDual_sub, ofDual_sub
|
instSubNegAddMonoid 📖 | CompOp | — |
instSubtractionMonoid 📖 | CompOp | — |
instVAdd 📖 | CompOp | 7 mathmath: toDual_vadd, instVAddAssocClass_1, instContinuousVAdd_right, instVAddCommClass_2, instContinuousConstVAddOrderDual, instVAddAssocClass_2, ofDual_vadd
|
instVAdd' 📖 | CompOp | 8 mathmath: toDual_vadd', instVAddCommClass_1, instVAddAssocClass_1, instContinuousVAdd_left, continuousConstVAdd', instVAddAssocClass, instVAddCommClass, ofDual_vadd'
|
instZero 📖 | CompOp | 14 mathmath: instIsRightCancelMulZero, instIsStrictOrderedModule, toDual_zero, toDual_eq_zero, instSMulPosStrictMono, instSMulPosReflectLE, instSMulPosMono, instSMulPosReflectLT, instIsOrderedModule, instIsCancelMulZero, instNoZeroDivisors, ofDual_zero, ofDual_eq_zero, instIsLeftCancelMulZero
|
| Name | Category | Theorems |
|---|
instAddCancelCommMonoidColex 📖 | CompOp | — |
instAddCancelCommMonoidLex 📖 | CompOp | — |
instAddCancelMonoidColex 📖 | CompOp | — |
instAddCancelMonoidLex 📖 | 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 | 42 mathmath: HahnEmbedding.Seed.baseEmbedding_pos, HahnEmbedding.IsPartial.baseEmbedding_le, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, HahnEmbedding.Partial.baseEmbedding_le_sSupFun, HahnEmbedding.Partial.archimedeanClassMk_eq_iff, HahnEmbedding.Partial.truncLT_mem_range_extendFun, HahnEmbedding.Seed.baseEmbedding_strictMono, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, HahnEmbedding.Partial.orderTop_eq_iff, HahnEmbedding.Partial.lt_extend, HahnEmbedding.Partial.coeff_eq_of_mem, HahnEmbedding.Partial.extendFun_strictMono, HahnEmbedding.IsPartial.strictMono, HahnEmbedding.Partial.exists_sub_mem_ball, HahnEmbedding.IsPartial.truncLT_mem_range, HahnEmbedding.Partial.truncLT_mem_range_sSupFun, HahnSeries.archimedeanClassMk_eq_archimedeanClassMk_iff, HahnEmbedding.Partial.le_sSupFun, HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_snd, HahnEmbedding.Seed.coeff_baseEmbedding, HahnSeries.archimedeanClassOrderIsoWithTop_apply, HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff_of_orderTop_ofLex, HahnEmbedding.Partial.coeff_eq_zero_of_mem, 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, HahnEmbedding.Partial.eval_lt, HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_fst, HahnEmbedding.Partial.archimedeanClassMk_le_of_eval_eq, HahnEmbedding.Partial.baseEmbedding_le_extendFun, HahnEmbedding.Partial.eval_eq_truncLT, HahnSeries.finiteArchimedeanClassOrderIso_apply, HahnEmbedding.Partial.evalCoeff_eq, HahnEmbedding.Partial.sSupFun_strictMono, HahnEmbedding.Partial.exists_domain_eq_top, HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun, HahnEmbedding.Partial.exists_isMax, HahnEmbedding.Partial.apply_of_mem_stratum, HahnEmbedding.Seed.domain_baseEmbedding, HahnEmbedding.Partial.toOrderAddMonoidHom_injective
|
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 | — |
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 | — |
instAddLeftCancelSemigroupColex 📖 | CompOp | — |
instAddLeftCancelSemigroupLex 📖 | 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 | — |
instAddRightCancelMonoidColex 📖 | CompOp | — |
instAddRightCancelMonoidLex 📖 | CompOp | — |
instAddRightCancelSemigroupColex 📖 | CompOp | — |
instAddRightCancelSemigroupLex 📖 | CompOp | — |
instAddSemigroupColex 📖 | CompOp | — |
instAddSemigroupLex 📖 | 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
|
instCancelCommMonoidColex 📖 | CompOp | — |
instCancelCommMonoidLex 📖 | CompOp | — |
instCancelMonoidColex 📖 | CompOp | — |
instCancelMonoidLex 📖 | CompOp | — |
instCommGroupColex 📖 | CompOp | — |
instCommGroupLex 📖 | CompOp | — |
instCommMonoidColex 📖 | CompOp | — |
instCommMonoidLex 📖 | CompOp | 3 mathmath: Prod.Lex.isOrderedCancelMonoid, Pi.Lex.isOrderedCancelMonoid, Prod.Lex.isOrderedMonoid
|
instCommSemigroupColex 📖 | CompOp | — |
instCommSemigroupLex 📖 | CompOp | — |
instDivColex 📖 | CompOp | 2 mathmath: ofColex_div, toColex_div
|
instDivInvMonoidColex 📖 | CompOp | — |
instDivInvMonoidLex 📖 | CompOp | — |
instDivLex 📖 | CompOp | 2 mathmath: toLex_div, ofLex_div
|
instDivisionAddCommMonoidColex 📖 | CompOp | — |
instDivisionAddCommMonoidLex 📖 | CompOp | — |
instDivisionCommMonoidColex 📖 | CompOp | — |
instDivisionCommMonoidLex 📖 | CompOp | — |
instDivisionMonoidColex 📖 | CompOp | — |
instDivisionMonoidLex 📖 | CompOp | — |
instGroupColex 📖 | CompOp | — |
instGroupLex 📖 | CompOp | — |
instInvColex 📖 | CompOp | 2 mathmath: toColex_inv, ofColex_inv
|
instInvLex 📖 | CompOp | 2 mathmath: toLex_inv, ofLex_inv
|
instInvolutiveInvColex 📖 | CompOp | — |
instInvolutiveInvLex 📖 | CompOp | — |
instInvolutiveNegColex 📖 | CompOp | — |
instInvolutiveNegLex 📖 | CompOp | — |
instLeftCancelMonoidColex 📖 | CompOp | — |
instLeftCancelMonoidLex 📖 | CompOp | — |
instLeftCancelSemigroupColex 📖 | CompOp | — |
instLeftCancelSemigroupLex 📖 | CompOp | — |
instMonoidColex 📖 | CompOp | — |
instMonoidLex 📖 | CompOp | — |
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
|
instNegColex 📖 | CompOp | 2 mathmath: toColex_neg, ofColex_neg
|
instNegLex 📖 | CompOp | 2 mathmath: ofLex_neg, toLex_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
|
instRightCancelMonoidColex 📖 | CompOp | — |
instRightCancelMonoidLex 📖 | CompOp | — |
instRightCancelSemigroupColex 📖 | CompOp | — |
instRightCancelSemigroupLex 📖 | CompOp | — |
instSemigroupColex 📖 | CompOp | — |
instSemigroupLex 📖 | CompOp | — |
instSubColex 📖 | CompOp | 2 mathmath: toColex_sub, ofColex_sub
|
instSubLex 📖 | CompOp | 2 mathmath: toLex_sub, ofLex_sub
|
instSubNegAddMonoidColex 📖 | CompOp | — |
instSubNegAddMonoidLex 📖 | CompOp | — |
instSubtractionMonoidColex 📖 | CompOp | — |
instSubtractionMonoidLex 📖 | 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
|