| Name | Category | Theorems |
|---|
instBEqColex 📖 | CompOp | 1 mathmath: instLawfulBEqColex
|
instBEqLex 📖 | CompOp | 1 mathmath: instLawfulBEqLex
|
instCoeFunColex 📖 | CompOp | — |
instCoeFunLex 📖 | CompOp | — |
instDecidableEqColex 📖 | CompOp | — |
instDecidableEqLex 📖 | CompOp | — |
instInhabitedColex 📖 | CompOp | — |
instInhabitedLex 📖 | CompOp | — |
instUniqueColex 📖 | CompOp | — |
instUniqueLex 📖 | CompOp | — |
ofColex 📖 | CompOp | 44 mathmath: toColex_symm_eq, isLeftRegular_ofColex, toColex_ofColex, ofColex_one, Finset.Colex.le_iff_max'_mem, ofColex_div, ofColex_add, Finset.Colex.lt_iff_exists_forall_lt, isAddLeftRegular_ofColex, ofColex_vadd', pow_ofColex, ofColex_smul', isAddRegular_ofColex, Pi.ofColex_apply, DFinsupp.colex_lt_iff_of_unique, Finset.geomSum_ofColex_strictMono, ofColex_mul, ofColex_eq_zero, ofColex_inv, DFinsupp.Colex.le_iff_of_unique, Finset.Colex.ofColex_top, DFinsupp.Colex.lt_iff, Finsupp.Colex.le_iff_of_unique, ofColex_inj, ofColex_smul, Finsupp.Colex.lt_iff, ofColex_symm_eq, ofColex_vadd, isAddRightRegular_ofColex, Finset.Colex.le_def, ofColex_pow, Finset.Colex.lt_iff_max'_mem, isRightRegular_ofColex, ofColex_eq_one, Finset.Colex.toColex_image_ofColex_strictMono, ofColex_sub, Finset.Colex.le_iff_sdiff_subset_lowerClosure, ofColex_neg, ofColex_toColex, Finset.orderIsoColex_symm_apply, Finsupp.Colex.lt_iff_of_unique, ofColex_zero, Finset.Colex.ofColex_bot, isRegular_ofColex
|
ofLex 📖 | CompOp | 112 mathmath: DFinsupp.lex_lt_iff_of_unique, Prod.Lex.lt_iff', ofLex_symm_eq, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, Prod.Lex.compare_def, Prod.Lex.monotone_fst, ofLex_add, isRightRegular_ofLex, ofLex_ratCast, Pi.ofLex_apply, ofLex_sub, MvPolynomial.supDegree_esymmAlgHomMonomial, ofLex_intCast, Prod.Lex.monotone_fst_ofLex, HahnSeries.support_abs, HahnEmbedding.Partial.truncLT_mem_range_extendFun, Prod.Lex.prodLexAssoc_symm_apply, ofLex_vadd, DFinsupp.lex_lt_iff, HahnEmbedding.Partial.orderTop_eq_iff, ofLex_pow, HahnEmbedding.Partial.coeff_eq_of_mem, Set.PartiallyWellOrderedOn.imageProdLex, Prod.Lex.sumLexProdLexDistrib_symm_apply, ofLex_eq_one, DFinsupp.Lex.le_iff_of_unique, HahnSeries.embDomainOrderEmbedding_apply, Prod.Lex.le_iff, HahnEmbedding.IsPartial.truncLT_mem_range, toLex_ofLex, HahnSeries.order_abs, ofLex_neg, ofLex_natCast, HahnEmbedding.Partial.truncLT_mem_range_sSupFun, coe_ofLexMulEquiv, Sum.Lex.toLexRelIsoLE_symm_coe, HahnSeries.archimedeanClassMk_eq_archimedeanClassMk_iff, Prod.Lex.sumLexProdLexDistrib_apply, ofLex_toLex, HahnSeries.leadingCoeff_pos_iff, Prod.Lex.uniqueProd_apply, OrderIso.sumLexCongr_apply, MvPolynomial.supDegree_esymm, Prod.Lex.covBy_iff, HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_snd, Finsupp.Lex.le_iff_of_unique, HahnEmbedding.Seed.coeff_baseEmbedding, Finsupp.lex_lt_iff_of_unique, ofLex_one, toLex_symm_eq, DFinsupp.Lex.lt_iff_of_unique, HahnSeries.archimedeanClassOrderIsoWithTop_apply, OrderMonoidHom.fstₗ_apply, HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff_of_orderTop_ofLex, Sum.Lex.lt_def, isAddRightRegular_ofLex, ofLex_inj, ofLex_inv, HahnEmbedding.Partial.coeff_eq_zero_of_mem, coe_ofLexAddEquiv, DFinsupp.lex_le_iff_of_unique, HahnSeries.leadingCoeff_nonneg_iff, toEquiv_ofLexMulEquiv, HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk, hahnEmbedding_isOrderedModule_rat, ofLex_ofNat, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, Finsupp.lex_le_iff_of_unique, ofLex_smul', HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff, pow_ofLex, ofLex_vadd', ofLex_smul, HahnSeries.lt_iff, Finsupp.lex_lt_iff, OrderAddMonoidHom.fstₗ_apply, isAddRegular_ofLex, HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_fst, HahnSeries.orderTop_abs, HVertexOperator.coeff_comp, ofLex_mul, Sum.Lex.le_def, HahnEmbedding.Partial.eval_eq_truncLT, HahnSeries.finiteArchimedeanClassOrderIso_apply, Prod.Lex.prodUnique_apply, isAddLeftRegular_ofLex, HahnEmbedding.Partial.evalCoeff_eq, MvPolynomial.IsSymmetric.antitone_supDegree, isLeftRegular_ofLex, MvPolynomial.leadingCoeff_toLex, HahnSeries.leadingCoeff_neg_iff, Sum.Lex.toLexRelIsoLT_symm_coe, ofLex_div, Prod.Lex.prodLexCongr_apply, Finsupp.Lex.lt_iff, HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun, isRegular_ofLex, ofLex_eq_zero, Prod.Lex.lt_iff, Prod.Lex.prodLexAssoc_apply, HahnSeries.leadingCoeff_nonpos_iff, WCovBy.fst_ofLex, Finsupp.Lex.lt_iff_of_unique, ofLex_zero, toEquiv_ofLexAddEquiv, hahnEmbedding_isOrderedAddMonoid, DFinsupp.Lex.lt_iff, HahnSeries.leadingCoeff_abs, coe_ofLexLinearEquiv, Set.PartiallyWellOrderedOn.ProdLex_iff, Prod.Lex.le_iff', hahnEmbedding_isOrderedModule
|
toColex 📖 | CompOp | 78 mathmath: toColex_symm_eq, Finset.Colex.toColex_le_singleton, Finset.geomSum_lt_geomSum_iff_toColex_lt_toColex, toColex_ofColex, toColex_sub, Finset.Colex.toColex_univ, Finsupp.toColex_monotone, pow_toColex, Pi.toColex_monotone, Pi.colex_asc, toColex_vadd, toColex_inv, toColex_add, Finset.Colex.toColex_lt_toColex_iff_max'_mem, Finset.Colex.cons_lt_cons, Finset.Colex.toColex_sdiff_le_toColex_sdiff', Colex.forall, Finset.Colex.toColex_strictMono, isAddRightRegular_toColex, Finset.Colex.mem_initSeg, Finset.geomSum_le_geomSum_iff_toColex_le_toColex, Finset.Colex.erase_lt_erase, Finset.Colex.erase_le_erase, Finset.Colex.toColex_le_toColex_iff_max'_mem, Finset.Colex.singleton_le_toColex, Finset.Colex.toColex_image_lt_toColex_image, toColex_eq_zero, Finset.Colex.toColex_sdiff_lt_toColex_sdiff, Finset.Colex.toColex_sdiff_le_toColex_sdiff, isRightRegular_toColex, toColex_one, Finset.Colex.lt_iff_exists_filter_lt, Finset.Colex.toColex_le_toColex, Finset.Colex.toColex_lt_singleton, Finset.Colex.singleton_lt_singleton, Pi.lt_toColex_update_self_iff, toColex_neg, toColex_smul, toColex_vadd', Finset.Colex.toColex_lt_toColex_iff_exists_forall_lt, Finset.Colex.insert_le_insert, Finset.Colex.toColex_mono, toColex_inj, Pi.toColex_apply, ofColex_symm_eq, Finset.UV.toColex_compress_lt_toColex, toColex_mul, Pi.toColex_strictMono, Finset.Colex.erase_le_erase_min', Pi.toColex_update_le_self_iff, Finset.Colex.toColex_lt_toColex_of_ssubset, Colex.exists, Finset.Colex.toColex_image_ofColex_strictMono, DFinsupp.toColex_monotone, isAddRegular_toColex, Finset.Colex.singleton_le_singleton, Finset.Colex.toColex_lt_toColex, Finset.Colex.toColex_image_le_toColex_image, Finset.Colex.toColex_sdiff_lt_toColex_sdiff', Finset.Colex.toColex_empty, Finsupp.Colex.single_le_iff, Finset.Colex.cons_le_cons, toColex_zero, toColex_div, Pi.le_toColex_update_self_iff, toColex_pow, isAddLeftRegular_toColex, Finsupp.Colex.single_lt_iff, ofColex_toColex, isRegular_toColex, toColex_eq_one, Finset.Colex.toColex_le_toColex_of_subset, Finset.orderIsoColex_apply, Finset.Colex.insert_lt_insert, toColex_smul', Finsupp.Colex.single_strictMono, Pi.toColex_update_lt_self_iff, isLeftRegular_toColex
|
toLex 📖 | CompOp | 166 mathmath: Prod.Lex.toLex_lt_toLex', toLex_sub, toLex_mul, Lex.forall, Sum.Lex.Icc_inr_inr, WithBot.orderIsoPUnitSumLex_symm_inl, isLeftRegular_toLex, Lex.exists, OrderIso.sumLexIicIoi_symm_apply_of_lt, toLex_inj, ofLex_symm_eq, Sum.Lex.Ico_inl_inl, Sum.Lex.Ico_inr_inr, MvPowerSeries.exists_finsupp_eq_lexOrder_of_ne_zero, pow_toLex, toLex_ofNat, Sum.Lex.Ioo_inl_inr, LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex, toEquiv_toLexMulEquiv, DFinsupp.toLex_monotone, toLex_eq_one, Sum.Lex.inr_le_inr_iff, WithBot.orderIsoPUnitSumLex_symm_inr, OrderIso.sumLexIioIci_symm_apply_Ici, Finsupp.Lex.single_strictAnti, Sum.Lex.Iic_inr, NonemptyInterval.toLex_strictMono, MvPolynomial.supDegree_esymmAlgHomMonomial, isRegular_toLex, Sum.Lex.inr_strictMono, Prod.Lex.toLexOrderHom_coe, Prod.Lex.toLex_le_toLex', HahnEmbedding.Partial.truncLT_mem_range_extendFun, Sum.Lex.Ioo_inr_inr, toLex_vadd', Sum.Lex.inl_bot, Prod.Lex.prodLexAssoc_symm_apply, MvPowerSeries.lexOrder_def_of_ne_zero, Pi.toLex_update_le_self_iff, Sum.Lex.toLex_lt_toLex, Pi.toLex_update_lt_self_iff, OrderIso.sumLexIicIoi_symm_apply_of_le, Sum.Lex.Icc_inl_inl, Pi.le_toLex_update_self_iff, WithTop.orderIsoSumLexPUnit_toLex, Sum.Lex.inl_mono, MvPolynomial.leadingCoeff_esymmAlgHomMonomial, Prod.Lex.sumLexProdLexDistrib_symm_apply, Sum.Lex.toLexRelIsoLE_coe, WithTop.orderIsoSumLexPUnit_symm_inl, Sum.Lex.Ioi_inr, HahnSeries.embDomainOrderEmbedding_apply, OrderIso.sumLexIioIci_symm_apply_Iio, HahnEmbedding.IsPartial.truncLT_mem_range, toLex_ofLex, Sum.Lex.Ici_inl, Sum.Lex.Ioc_inl_inl, coe_toLexLinearEquiv, toLex_add, isAddLeftRegular_toLex, OrderMonoidHom.inrₗ_apply, Pi.lex_desc, HahnEmbedding.Partial.truncLT_mem_range_sSupFun, Sum.Lex.toLex_le_toLex, toLex_pow, Finsupp.Lex.single_lt_iff, OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex, toLex_ratCast, Sum.Lex.Ioc_inl_inr, Sum.Lex.Iio_inl, toLex_intCast, Prod.Lex.sumLexProdLexDistrib_apply, isAddRightRegular_toLex, ofLex_toLex, WithTop.orderIsoSumLexPUnit_top, toLex_zero, OrderIso.sumLexCongr_apply, MvPolynomial.supDegree_esymm, Prod.Lex.toLex_lt_toLex, Sum.Lex.Ioc_inr_inr, Finsupp.DegLex.lt_iff, MvPolynomial.leadingCoeff_toLex_C, Sum.Lex.Ioi_inl, Sum.Lex.Ioo_inl_inl, MvPolynomial.monic_esymm, isAddRegular_toLex, OrderIso.sumLexIicIoi_apply_inr, Set.PartiallyWellOrderedOn.fiberProdLex, toLex_natCast, Sum.Lex.Iic_inl, Sum.Lex.inl_strictMono, toLex_symm_eq, MvPolynomial.supDegree_toLex_C, isRightRegular_toLex, toLex_inv, OrderMonoidHom.inlₗ_apply, Sum.Lex.Ici_inr, Sum.Lex.inl_lt_inl_iff, OrderIso.sumLexAssoc_apply_inl_inl, toLex_vadd, OrderAddMonoidHom.inlₗ_apply, OrderIso.sumLexEmpty_apply_inl, OrderIso.sumLexIicIoi_apply_inl, Sum.Lex.Ico_inl_inr, Sum.Lex.Iio_inr, Sum.Lex.toLexRelIsoLT_coe, Pi.toLex_apply, OrderAddMonoidHom.inlₗ_add_inrₗ_eq_toLex, Pi.lt_toLex_update_self_iff, WithBot.orderIsoPUnitSumLex_toLex, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, toLex_smul', Prod.Lex.toLex_mono, OrderIso.emptySumLex_apply_inr, Sum.Lex.inl_lt_inr, Finsupp.Lex.single_antitone, OrderIso.sumLexIioIci_symm_apply_of_ge, Prod.Lex.toLex_covBy_toLex_iff, coe_toLexMulEquiv, Prod.Lex.toLex_strictMono, NonemptyInterval.toLex_mono, MonomialOrder.lex_lt_iff, OrderIso.sumLexIioIci_apply_inl, Sum.Lex.inr_mono, WithTop.orderIsoSumLexPUnit_symm_inr, OrderIso.sumLexAssoc_apply_inr, NonemptyInterval.toLex_lt_toLex, Sum.Lex.not_inr_le_inl, Finsupp.DegLex.le_iff, HahnEmbedding.Partial.eval_eq_truncLT, toEquiv_toLexAddEquiv, toLex_eq_zero, MonomialOrder.lex_le_iff, toLex_div, MvPolynomial.IsSymmetric.antitone_supDegree, Sum.Lex.inr_top, MvPolynomial.leadingCoeff_toLex, Prod.Lex.toLex_le_toLex, MvPowerSeries.lexOrder_le_of_coeff_ne_zero, Finsupp.toLex_monotone, Sum.Lex.toLex_strictMono, Prod.Lex.prodLexCongr_apply, Sum.Lex.inr_lt_inr_iff, Finsupp.Lex.single_le_iff, HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun, OrderAddMonoidHom.inrₗ_apply, Finsupp.DegLex.lt_def, Prod.Lex.prodLexAssoc_apply, Sum.Lex.Icc_inl_inr, HahnEmbedding.Partial.apply_of_mem_stratum, toLex_smul, toLex_one, coe_toLexAddEquiv, OrderIso.sumLexIioIci_apply_inr, OrderIso.sumLexIioIci_symm_apply_of_lt, OrderIso.sumLexAssoc_apply_inl_inr, Sum.Lex.toLex_mono, Pi.toLex_strictMono, NonemptyInterval.toLex_le_toLex, toLex_neg, Sum.Lex.not_inr_lt_inl, WithBot.orderIsoPUnitSumLex_bot, Set.PartiallyWellOrderedOn.ProdLex_iff, Sum.Lex.inl_le_inr, Sum.Lex.inl_le_inl_iff, Pi.toLex_monotone
|