| Name | Category | Theorems |
|---|
Le 📖 | MathDef | — |
attach 📖 | CompOp | 23 mathmath: attach_ndinsert, count_attach, attach_map_val', Sym.attach_mk, attach_map_val, card_attach, countP_attach, attach_cons, filter_attach, mem_attach, Nodup.attach, erase_attach_map, Finset.attach_val, Finsupp.supportedEquivFinsupp_apply_support_val, attach_zero, KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map, attach_bind_coe, coe_attach, Sym.coe_attach, erase_attach_map_val, nodup_attach, filter_attach', pmap_eq_map_attach
|
card 📖 | CompOp | 175 mathmath: card_eq_zero, Ideal.pow_multiset_sum_mem_span_pow, countP_le_card, card_eq_countP_add_countP, IsNonarchimedean.multiset_powerset_image_add, Polynomial.card_roots_le_map, Sym.val_eq_coe, prod_X_sub_X_eq_sum_esymm, Equiv.Perm.sign_of_cycleType, prod_map_neg, noncommSum_eq_card_nsmul, card_filter_le_iff, Polynomial.card_roots_sub_C', sum_count_eq_card, card_pi, powersetCard_card_add, Polynomial.map_sub_roots_sprod_eq_prod_map_eval, vadd_sum, card_eq_three, card_Ioc_eq_card_Icc_sub_one, toFinset_sum_count_eq, IsAlgClosed.card_roots_eq_natDegree, dedup_card_eq_card_iff_nodup, PMF.toMeasure_ofMultiset_apply, mem_powersetCardAux, MvPolynomial.totalDegree_eq, toFinsupp_sum_eq, card_Ico_eq_card_Icc_sub_one, Polynomial.natDegree_eq_card_roots', card_replicate, mem_powersetCard, Polynomial.card_roots_le_derivative, Finsupp.card_toMultiset, eq_replicate_of_mem, toFinset_card_le, Finset.map_sym_eq_piAntidiag, card_add, Cubic.splits_iff_card_roots, Polynomial.card_roots_map_le_degree, sup_powerset_len, card_le_card, count_eq_card_filter_eq, sum_le_card_nsmul, CovBy.card_multiset, Polynomial.Splits.degree_eq_card_roots, card_range, IsAlgClosed.card_roots_map_eq_natDegree_of_isUnit_leadingCoeff, countP_True, length_ndinsert_of_notMem, card_nsmul_le_sum, card_erase_add_one, card_erase_eq_ite, length_toList, map_const, Polynomial.card_nthRoots, cardHom_apply, card_nsmul, IsAlgClosed.card_roots_map_eq_natDegree_from_simpleRing, multinomial_filter_ne, card_le_card_toFinset_add_one_iff, Equiv.Perm.card_cycleType_eq_one, card_nthRoots_subgroup_units, card_eq_four, PMF.toOuterMeasure_ofMultiset_apply, map_count_True_eq_filter_card, Equiv.Perm.card_cycleType_pos, pow_card_le_prod, Sym2.card_toMultiset, card_attach, Finset.sum_pow_of_commute, Polynomial.exists_multiset_roots, card_singleton, card_powersetCard, card_erase_le, AlternatingGroup.card_of_cycleType, Polynomial.splits_iff_card_roots, Associated.card_factors_eq, card_cons, countP_map, MvPolynomial.totalDegree_le_degrees_card, IsAlgClosed.card_aroots_eq_natDegree, rel_replicate_left, noncommProd_eq_pow_card, prod_map_le_pow_card, Polynomial.card_roots_le_one_of_irreducible, Polynomial.card_roots', Polynomial.card_roots_X_pow_sub_C, card_antidiagonal, count_le_card, length_ndinsert_of_mem, IsAlgClosed.card_aroots_eq_natDegree_of_leadingCoeff_ne_zero, Polynomial.Splits.natDegree_eq_card_roots, card_product, Polynomial.natDegree_multiset_prod_X_sub_C_eq_card, card_zero, card_pmap, card_sum, Polynomial.card_roots_map_le_natDegree, card_mono, count_map, card_Ioo_eq_card_Icc_sub_two, card_toFinset, length_sort, card_erase_of_mem, Equiv.Perm.card_cycleType_eq_zero, IsAlgClosed.card_roots_map_eq_natDegree_of_injective, toFinset_card_eq_one_iff, eq_replicate, grade_eq, card_eq_two, Polynomial.card_roots, Polynomial.degree_eq_card_roots, toFinset_card_of_nodup, Cycle.card_toMultiset, Equiv.Perm.cycleType_of_pow_prime_eq_one, card_pos, card_powerset, IsAlgClosed.card_roots_map_eq_natDegree_of_leadingCoeff_ne_zero, toFinset_card_eq_card_iff_nodup, IsAlgClosed.card_aroots_eq_natDegree_of_isUnit_leadingCoeff, Sym.oneEquiv_apply, Finset.card_mk, card_sections, card_eq_one, coe_card, IsPrimitiveRoot.card_nthRoots_one, Polynomial.card_roots_le_map_of_injective, countP_eq_card, UniqueFactorizationMonoid.card_factors_of_irreducible, card_join, card_erase_lt_of_mem, Finset.card_def, prod_X_add_C_eq_sum_esymm, rel_replicate_right, card_lt_card, Polynomial.exists_prod_multiset_X_sub_C_mul, Polynomial.degree_eq_card_roots', Finset.card_val, card_pos_iff_exists_mem, Finset.sum_pow, card_finsuppSum, card_toEnumFinset, card_disjSum, eq_replicate_card, count_eq_card, card_pair, countP_eq_card_filter, IsPrimitiveRoot.card_nthRoots, Polynomial.natDegree_eq_card_roots, AlternatingGroup.map_subtype_of_cycleType, card_eq_card_of_rel, smul_prod, Nat.filter_multiset_Ico_card_eq_of_periodic, bind_powerset_len, map_const', card_bind, prod_le_pow_card, Polynomial.coeff_multiset_prod_of_natDegree_le, card_coe, card_sub, Polynomial.card_roots_sub_C, Sym.val_replicate, AlternatingGroup.card_of_cycleType_mul_eq, card_map, card_strictMono, PMF.ofMultiset_apply, Squarefree.moebius_eq, Nat.card_antidiagonal, Polynomial.roots_def, card_sym2, card_sigma, toFinset_eq_singleton_iff, PrimeMultiset.card_ofPrime, Sym.card_coe, card_Ioo_eq_card_Ico_sub_one
|
decidableDexistsMultiset 📖 | CompOp | — |
decidableDforallMultiset 📖 | CompOp | 4 mathmath: Equiv.Perm.card_of_cycleType_mul_eq, Equiv.Perm.card_of_cycleType, AlternatingGroup.card_of_cycleType, AlternatingGroup.card_of_cycleType_mul_eq
|
decidableEq 📖 | CompOp | 9 mathmath: Equiv.Perm.card_of_cycleType_mul_eq, sup_powerset_len, AlternatingGroup.card_of_cycleType_singleton, Equiv.Perm.card_of_cycleType_eq_zero_iff, Equiv.Perm.card_of_cycleType, AlternatingGroup.card_of_cycleType, Equiv.Perm.card_of_cycleType_singleton, AlternatingGroup.map_subtype_of_cycleType, AlternatingGroup.card_of_cycleType_mul_eq
|
decidableEqPiMultiset 📖 | CompOp | — |
decidableExistsMultiset 📖 | CompOp | — |
decidableForallMultiset 📖 | CompOp | — |
decidableLE 📖 | CompOp | — |
decidableMem 📖 | CompOp | 5 mathmath: card_erase_eq_ite, count_dedup, count_eq_of_nodup, max_norm_root_eq_spectralValue, filter_attach'
|
instCoeList 📖 | CompOp | — |
instDecidableEquivListOfDecidableEq 📖 | CompOp | — |
instDecidableRListOfDecidableEq 📖 | CompOp | — |
instHasSSubset 📖 | CompOp | 6 mathmath: isWellFounded_ssubset, ssubset_singleton_iff, ssubset_cons, instIsNonstrictStrictOrder, toFinset_ssubset, zero_ssubset
|
instHasSubset 📖 | CompOp | 34 mathmath: le_iff_subset, subset_of_le, coe_subset, Ico_subset_Ico_iff, cons_subset, filter_subset, subset_ndunion_left, MvPolynomial.degrees_rename, range_subset, le_ndinter, ndunion_le, subset_ndunion_right, Finset.subset_def, Subset.refl, instIsNonstrictStrictOrder, zero_subset, singleton_subset, subset_iff, subset_zero, subset_cons, replicate_subset_singleton, subset_dedup', subset_add_left, ndinter_subset_left, subset_add_right, toFinset_subset, subset_dedup, ndinter_subset_right, erase_subset, dedup_subset', dedup_subset, Finset.val_le_iff_val_subset, UniqueFactorizationMonoid.radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors, Le.subset
|
instMembership 📖 | CompOp | 224 mathmath: dedup_ext, Polynomial.mem_aroots', Finset.pimage_eq_image_filter, Finmap.lookup_eq_some_iff, exists_associated_mem_of_dvd_prod, erase_lt, lcm_eq_zero_iff, Nodup.notMem, IsNonarchimedean.multiset_powerset_image_add, attach_ndinsert, isConjRoot_iff_mem_minpoly_aroots, UniqueFactorizationMonoid.mem_normalizedFactors_iff, Polynomial.mem_roots_sub_C', notMem_zero, card_filter_le_iff, Polynomial.zero_notMem_multiset_map_X_sub_C, count_attach, mem_powerset, mem_coe, mem_union, Finset.mem_mk, mem_sigma, IsUltrametricDist.exists_norm_multiset_prod_le, cons_subset, Finset.mem_sum, Prime.exists_mem_multiset_map_dvd, mem_pi, inr_mem_disjSum, coe_mem, Cubic.mem_roots_iff, mem_sub_of_nodup, disjoint_singleton, attach_map_val', mem_rootsOfUnity_iff_mem_nthRoots, mem_powersetCard, left_notMem_Ioo, Finset.mk_cons, UniqueFactorizationMonoid.exists_mem_factors, eq_zero_iff_forall_notMem, mem_map, Cycle.mem_lists_iff_coe_eq, Prime.exists_mem_multiset_dvd, Nat.mem_antidiagonalTuple, Nat.mem_antidiagonal, Sym.attach_mk, setOf_mem_sym2, normalizedFactorsEquivOfQuotEquiv_symm, mem_ndinsert, Ideal.IsPrime.multiset_prod_map_le, Sym.mem_mk, IsNonarchimedean.multiset_image_add_of_nonempty, Polynomial.mem_roots_map_of_injective, mem_sup_map_support_iff, Finmap.mem_def, Finset.mem_univ_val, right_notMem_Ico, attach_map_val, prod_eq_zero_iff, card_erase_eq_ite, mem_antidiagonal, mem_erase_of_ne, mk_mem_sym2_iff, Finset.noncommProd_lemma, Associates.mem_factorSet_some, mem_dedup, IsUltrametricDist.exists_norm_multiset_sum_le, nodup_cons, inl_mem_disjSum, Finsupp.mem_toMultiset, Equiv.Perm.mem_cycleType_iff, mem_add, UniqueFactorizationMonoid.exists_mem_normalizedFactors, mem_sym2_iff, mem_disjSum, mem_range, left_notMem_Ioc, exists_max_image, IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime, left_mem_Ico, mem_ndunion, mem_sections, card_attach, Finset.sum_pow_of_commute, count_ne_zero, countP_attach, Ideal.IsPrime.multiset_prod_le, Finset.noncommSum_insert_of_notMem, mem_map_of_injective, finite_toSet, count_pos, right_mem_Icc, iSup_mem_map_of_ne_zero, attach_cons, Finset.noncommSum_insert_of_notMem', Finset.noncommSum_cons, Associates.mem_factors'_iff_dvd, Algebra.IsAlgebraic.lift_cardinalMk_le_sigma_polynomial, mem_filterMap, filter_attach, mem_nsmul, mem_lists_iff, UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd, count_dedup, mem_cons, Ideal.IsPrime.multiset_prod_mem_iff_exists_mem, Polynomial.mem_roots_sub_C, mem_Ioi, Finmap.mem_lookup_iff, Algebra.IsAlgebraic.cardinalMk_le_sigma_polynomial, Polynomial.mem_roots_iff_aeval_eq_zero, UniqueFactorizationMonoid.mem_primeFactors, disjoint_left, Ideal.mem_normalizedFactors_iff, mem_replicate, Finsupp.mem_support_multiset_sum, mem_Ioc, Associates.exists_mem_multiset_le_of_prime, mem_attach, Sym2.mem_toMultiset, singleton_subset, mem_sort, mem_singleton, mem_sup, IntermediateField.algHomAdjoinIntegralEquiv_symm_apply_gen, notMem_range_self, PrimeMultiset.mem_ofNatMultiset, exists_min_image, disjoint_cons_left, Finset.noncommProd_cons', SimpleGraph.ComponentCompl.infinite_iff_in_all_ranges, subset_iff, Polynomial.mem_roots, Nodup.attach, Ideal.mem_primesOver_iff_mem_normalizedFactors, Polynomial.mem_roots', mem_Ioo, emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity, count_eq_of_nodup, disjoint_cons_right, erase_attach_map, Nodup.mem_erase_iff, Polynomial.mem_roots_map, mem_Iio, Polynomial.mem_normalizedFactors_iff, FractionalOperation.IsValid.contains, mem_toList, finite_toSet_toFinset, Nodup.ext, mem_bind, disjoint_ndinsert_right, Polynomial.mem_aroots, max_norm_root_eq_spectralValue, PowerBasis.liftEquiv'_apply_coe, mem_nsmul_of_ne_zero, countP_pos, mem_Iic, mem_singleton_self, mem_sub, Relation.cutExpand_iff, right_notMem_Ioo, UniqueFactorizationMonoid.mem_normalizedFactors_iff', ndinsert_le, mem_filter, rootsOfUnityEquivNthRoots_apply, Finset.noncommProd_insert_of_notMem', mem_sum, attach_zero, KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map, disjoint_right, attach_bind_coe, MvPolynomial.mem_degrees, mem_join, NumberField.mem_multisetInfinitePlace, exists_mem_of_ne_zero, IsNonarchimedean.multiset_image_add, mem_Icc, Sym.mem_coe, PowerBasis.liftEquiv'_symm_apply_apply, Nodup.notMem_erase, Finset.noncommSum_cons', PNat.mem_factorMultiset, mem_cons_self, count_eq_zero, add_singleton_eq_iff, right_mem_Ioc, card_pos_iff_exists_mem, Ideal.multiset_prod_eq_bot, Polynomial.mem_nthRoots, singleton_le, left_mem_Icc, gcd_ne_zero_iff, mem_Ici, mem_of_mem_toEnumFinset, lcm_ne_zero_iff, rootsOfUnityEquivNthRoots_symm_apply, Polynomial.zero_notMem_multiset_map_X_add_C, self_mem_range_succ, one_le_count_iff_mem, PrimeMultiset.mem_ofNatList, mem_toFinset, UniqueFactorizationMonoid.zero_notMem_normalizedFactors, erase_attach_map_val, empty_or_exists_mem, Finset.noncommProd_insert_of_notMem, nodup_attach, Associates.mem_factors'_of_dvd, disjoint_ndinsert_left, mem_ndinter, filter_attach', NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, singleton_disjoint, mem_Ico, Finset.noncommSum_lemma, Finset.mem_val, Finset.mem_def, mem_ndinsert_self, mem_pmap, pmap_eq_map_attach, Finset.noncommProd_cons, mem_product, map_eq_cons, UniqueFactorizationMonoid.exists_mem_factors_of_dvd, mem_inter, Polynomial.toSubring_one
|
instPartialOrder 📖 | CompOp | 189 mathmath: Finset.val_strictMono, ndunion_le_union, sub_le_self, le_iff_subset, coe_le, covBy_iff, MvPolynomial.degrees_monomial, disjoint_finset_sum_left, erase_lt, Finsupp.toMultiset_strictMono, le_singleton, CovBy.finset_val, le_iff_count, union_le_iff, UniqueFactorizationMonoid.disjoint_normalizedFactors, Finset.val_lt_iff, card_Ico, mem_powerset, Icc_eq, lt_iff_cons_le, Finset.ordConnected_range_val, isAtom_singleton, sub_le_iff_le_add', mem_powersetCardAux, instIsOrderedCancelAddMonoid, disjoint_add_left, range_disjoint_map_add, disjoint_singleton, le_ndinsert_self, le_dedup, mem_powersetCard, instCanonicallyOrderedAdd, disjSum_strictMono_left, Associates.prod_le_prod_iff_le, add_le_add_iff_right, add_eq_union_iff_disjoint, disjoint_list_sum_left, prod_X_sub_C_dvd_iff_le_roots, instExistsAddOfLE, disjoint_union_left, finset_sum_eq_sup_iff_disjoint, nodup_bind, UniqueFactorizationMonoid.normalizedFactors_pos, card_Ioc, le_dedup_self, le_union_right, map_fst_le_of_subset_toEnumFinset, UniqueFactorizationMonoid.factors_pos, le_add_sub, add_le_add_iff_left, DFinsupp.toMultiset_le_toMultiset, MvPolynomial.degrees_pow_le, monotone_filter_right, replicate_le_replicate, ndinter_le_left, Associates.factors_le, Polynomial.map_roots_le, map_single_le_powerset, disjoint_finset_sum_right, instAddLeftMono, toEnumFinset_subset_iff, le_add_left, MvPolynomial.degrees_map_le, disjSum_mono_right, bot_eq_zero, disjoint_sum_left, le_ndinter, MvPolynomial.degrees_indicator, Associates.factors_mono, le_inter_iff, ndunion_le, MvPolynomial.degrees_sub_le, le_cons_erase, le_union_left, instWellFoundedLT, disjoint_map_map, MvPolynomial.degrees_sum_le, filter_le, sub_le_iff_le_add, Nodup.add_iff, Polynomial.roots_expand_pow_map_iterateFrobenius_le, nodup_iff_le, cons_le_of_notMem, Polynomial.map_roots_le_of_injective, pairwise_disjoint_powersetCard, Polynomial.Splits.dvd_iff_roots_le_roots, disjoint_left, map_mono, MvPolynomial.mem_degreesLE, Finsupp.coe_orderIsoMultiset_symm, inter_le_ndinter, ndunion_le_add, dedup_le, card_mono, MvPolynomial.degrees_prod_le, disjoint_toFinset, Ico_disjoint_Ico, le_ndunion_left, lt_cons_self, MvPolynomial.degrees_add_le, map_le_map_iff, MvPolynomial.degrees_mul_le, disjoint_cons_left, grade_eq, disjoint_union_right, Finset.disjoint_val, inter_le_right, monotone_filter_left, Polynomial.roots.le_of_dvd, ZMod.erdos_ginzburg_ziv_multiset, Finset.grade_multiset_eq, mapEmbedding_apply, Nodup.le_nsmul_iff_le, disjoint_cons_right, cons_lt_cons_iff, union_le_add, UniqueFactorizationMonoid.le_emultiplicity_iff_replicate_le_normalizedFactors, zero_disjoint, inter_le_left, disjoint_ndinsert_right, le_zero, erase_le_iff_le_cons, toDFinsupp_le_toDFinsupp, map_strictMono, coe_disjoint, Equiv.Perm.cycleType_le_of_mem_cycleFactorsFinset, WCovBy.finset_val, card_Iic, le_count_iff_replicate_le, UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors, ndinsert_le, le_cons_self, instOrderedSub, Finset.val_wcovBy_val, range_le, le_replicate_iff, MvPolynomial.degrees_X', disjoint_right, le_sub_add, le_add_right, card_Icc, powersetCard_le_powerset, lt_singleton, Int.erdos_ginzburg_ziv_multiset, erase_le, toDFinsupp_lt_toDFinsupp, disjoint_of_nodup_add, covBy_cons, zero_le, ndinter_le_right, singleton_le, Nodup.le_dedup_iff_le, le_cons_of_notMem, disjoint_add_right, le_smul_dedup, DFinsupp.toMultiset_lt_toMultiset, le_iff_exists_add, replicate_mono, replicate_le_coe, Associates.prod_le, cons_le_cons_iff, mem_powersetAux, ndinter_eq_zero_iff_disjoint, disjSum_strictMono_right, card_Ioo, le_ndunion_right, disjoint_list_sum_right, le_filter, Finset.val_le_iff_val_subset, isAtom_iff, lt_replicate_succ, disjoint_ndinsert_left, disjoint_sum_right, toFinsupp_strictMono, instAddLeftReflectLE, Finset.val_le_iff, singleton_disjoint, disjoint_iff_ne, Polynomial.roots_expand_map_frobenius_le, Finsupp.coe_orderIsoMultiset, IsAlgClosed.dvd_iff_roots_le_roots, inter_eq_zero_iff_disjoint, monotone_sym2, le_bind, UniqueFactorizationMonoid.dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors, nodup_add, card_strictMono, disjSum_mono_left, Finset.val_covBy_val
|
instSizeOf 📖 | CompOp | — |
nodupDecidable 📖 | CompOp | — |
ofList 📖 | CompOp | 105 mathmath: powersetCardAux_eq_map_coe, Fin.univ_map_def, coe_le, coe_inter, coe_product, revzip_powersetAux, AList.toFinmap_entries, coe_subset, powerset_coe', filterMap_coe, coe_add, coe_toList, coe_subsingletonEquiv, Equiv.Perm.cycleType_eq, antidiagonal_coe', coe_count, mem_coe, coe_bind, coe_eq_zero, Cycle.coe_toMultiset, mem_powersetCardAux, Finset.sort_eq, Fin.univ_def, coe_countP, sup_coe, Nat.uIcc_eq_range', coe_foldl, coe_foldr, coe_ndinter, quot_mk_to_coe, coe_ndinsert, Nat.Ioc_eq_range', coe_sigma, powersetCard_coe, powerset_coe, coe_keys, Nat.Partition.ofComposition_parts, coe_range, lists_coe, coe_nodup, sum_coe, coe_eq_coe, inf_coe, Pi.cons_coe, antidiagonal_coe, coe_ndunion, PrimeMultiset.toPNatMultiset_ofPNatList, Finset.coe_toList, List.toFinset_coe, SimpleGraph.Walk.coe_support_append, Nat.factors_eq, Cycle.lists_coe, coe_sub, quot_mk_to_coe', pairwise_coe_iff, coe_sections, Nat.Ico_eq_range', coe_eq_singleton, powersetAux_eq_map_coe, coe_dedup, Polynomial.roots_list_prod, Nat.factorization_eq_primeFactorsList_multiset, coe_nodupKeys, revzip_powersetAux', coe_sort, List.toFinset_val, sort_eq, Finmap.keys_val, coe_disjoint, coe_fold_l, filter_coe, map_comp_coe, PNat.coeNat_factorMultiset, coe_card, Nat.Icc_eq_range', coe_fold_r, coe_pmap, coe_erase, cons_coe, Nat.val_divisorsAntidiagonal, lift_coe, coe_singleton, Finset.val_univ_fin, pi_coe, List.toFinset_eq, powersetCard_coe', map_coe, coe_reverse, coe_replicate, coe_foldr_swap, FreeRing.coe_eq, prod_coe, replicate_le_coe, mem_powersetAux, pairwise_coe_iff_pairwise, coe_attach, Nat.Ioo_eq_range', SimpleGraph.Walk.coe_support_append', quot_mk_to_coe'', sym2_coe, SimpleGraph.Walk.coe_support, coe_join, Fin.univ_val_map, coe_nil, coe_eq_zero_iff_isEmpty
|
pmap 📖 | CompOp | 10 mathmath: pmap_eq_map, Nodup.pmap, pmap_congr, card_pmap, map_pmap, pmap_cons, pmap_zero, coe_pmap, mem_pmap, pmap_eq_map_attach
|
sizeOf 📖 | CompOp | — |