| Name | Category | Theorems |
|---|
instLE 📖 | CompOp | 44 mathmath: MvPolynomial.dvd_monomial_one_iff_exists, instCanonicallyOrderedAddOfAddLeftMono, MvPowerSeries.coeff_mul_monomial, mapDomain_le_mapDomain_iff_le, coe_le_coe, mapDomain_nonneg, Nat.factorization_le_factorization_mul_left, MvPowerSeries.coeff_monomial_mul, bot_eq_zero, Nat.coe_divisors_eq_prod_pow_le_factorization, MvPowerSeries.LinearTopology.basis_le_iff, MonomialOrder.div_single, mapDomain_nonpos, le_def, le_iff, StdSimplex.nonneg, exists_le_degree_eq, isLowerSet_range_embDomain, MvPolynomial.dvd_monomial_iff_exists, single_le_single, MvPolynomial.coeff_monomial_mul', MvPowerSeries.coeff_trunc', single_nonpos, lt_def, orderEmbeddingToFun_apply, Nat.factorization_le_iff_dvd, Nat.dvd_iff_exists_le_factorization, coe_orderIsoMultiset_symm, wellQuasiOrderedLE, MvPolynomial.dvd_monomial_mul_iff_exists, MonomialOrder.div_set, le_iff', Nat.factorization_le_factorization_mul_right, addLeftReflectLE, single_le_iff, MvPolynomial.monomial_one_dvd_monomial_one, orderedSub, MonomialOrder.div, MvPolynomial.mem_ideal_span_monomial_image, MvPolynomial.coeff_mul_monomial', single_nonneg, embDomain_le_embDomain_iff_le, coe_orderIsoMultiset, MvPolynomial.monomial_dvd_monomial
|
lattice 📖 | CompOp | 1 mathmath: card_uIcc
|
orderEmbeddingToFun 📖 | CompOp | 1 mathmath: orderEmbeddingToFun_apply
|
orderIsoFunOnFinite 📖 | CompOp | — |
partialorder 📖 | CompOp | 18 mathmath: HahnSeries.instNoZeroDivisorsFinsuppNat, floorDiv_def, coe_ceilDiv_def, disjoint_iff, HahnSeries.toMvPowerSeries_symm_apply_coeff, floorDiv_apply, ceilDiv_apply, ceilDiv_def, Nat.ceilRoot_def, support_ceilDiv_subset, Nat.factorization_ceilRoot, support_floorDiv_subset, HahnSeries.coeff_toMvPowerSeries_symm, Nat.factorization_floorRoot, coe_floorDiv, Nat.floorRoot_def, HahnSeries.coeff_toMvPowerSeries, HahnSeries.toMvPowerSeries_apply
|
preorder 📖 | CompOp | 54 mathmath: instSMulPosReflectLE, MvPowerSeries.WithPiTopology.tendsto_trunc_atTop, Nat.coe_properDivisors_eq_prod_pow_lt_factorization, instPosSMulReflectLE, MvPowerSeries.eq_iff_frequently_trunc'_eq, card_Ioc, toMultiset_strictMono, card_Ico, toColex_monotone, isOrderedAddMonoid, MvPolynomial.pow_idealOfVars, MvPolynomial.idealOfVars_eq_restrictSupportIdeal, MonomialOrder.toSyn_strictMono, isOrderedCancelAddMonoid, Nat.properDivisors_eq_image_Iio_factorization_prod_pow, MvPowerSeries.coeff_inv, mapDomain_mono, card_Icc, instSMulPosReflectLT, card_Ioo, mapDomain_lt_mapDomain_iff_lt, instSMulPosMono, Nat.divisors_eq_map_attach_Iic_factorization_prod_pow, coe_strictMono, instPosSMulStrictMono, wellFoundedLT', isPWO, single_mono, MonomialOrder.toSyn_monotone, MvPowerSeries.coeff_inv_aux, lt_def, MvPowerSeries.coeff_trunc, embDomain_lt_embDomain_iff_lt, Nat.Iio_factorization_prod_pow_injective, instPosSMulMono, wellFoundedLT, instSMulPosStrictMono, MvPowerSeries.coeff_invOfUnit, coe_lt_coe, card_Iic, MvPowerSeries.WithPiTopology.tendsto_trunc'_atTop, card_Iio, Icc_eq, Nat.properDivisors_eq_map_attach_Iio_factorization_prod_pow, embDomain_mono, support_monotone, degree_mono, toLex_monotone, coe_mono, wellFoundedLT_of_finite, Multiset.toFinsupp_strictMono, lt_wf, Nat.Iic_factorization_prod_pow_injective, Nat.divisors_eq_image_Iic_factorization_prod_pow
|
semilatticeInf 📖 | CompOp | 7 mathmath: Multiset.toFinsupp_inter, inf_apply, support_inf_union_support_sup, support_sup_union_support_inf, support_inf, Nat.factorization_gcd, toMultiset_inf
|
semilatticeSup 📖 | CompOp | 17 mathmath: MonomialOrder.sPolynomial_leadingTerm_mul', Multiset.toFinsupp_union, MonomialOrder.sPolynomial_def, Nat.factorization_lcm, MonomialOrder.sPolynomial_monomial_mul, sup_apply, support_inf_union_support_sup, MonomialOrder.sPolynomial_monomial_mul', support_sup, MonomialOrder.degree_sPolynomial_le, MonomialOrder.coeff_sPolynomial_sup_eq_zero, support_sup_union_support_inf, toMultiset_sup, MonomialOrder.degree_sPolynomial_lt_sup_degree, MonomialOrder.sPolynomial_mul_monomial, MonomialOrder.sPolynomial_leadingTerm_mul, MonomialOrder.degree_sPolynomial
|