| Name | Category | Theorems |
|---|
cons 📖 | CompOp | 131 mathmath: fold_cons_left, product_cons, covBy_iff, dedup_cons, pi_cons, ndinsert_of_notMem, sup_cons, singleton_add, filter_cons, toFinset_cons, lt_iff_cons_le, map_cons, cons_subset, cons_swap, Finmap.entries_insert_of_notMem, Pi.cons_swap, consEquiv_symm_some, map_comp_cons, countP_cons, prod_cons, Finset.insert_val_of_notMem, fold_cons'_left, nsmul_cons, ndinter_cons_of_notMem, mem_cons_of_mem, antidiagonal_cons, replicate_succ, exists_cons_of_mem, rel_cons_left, sort_cons, cons_union_distrib, Finset.cons_val, count_cons, powersetCard_cons, not_nodup_pair, CovBy.exists_multiset_cons, nodup_cons, cons_ndunion, add_cons, Nat.antidiagonal_succ, Finset.insert_val', Nat.antidiagonal_succ', cons_eq_cons, cons_inter_of_pos, cons_add, DirectSum.addEquivProdDirectSum_symm_apply_support', le_cons_erase, ssubset_cons, lcm_cons, sections_cons, card_cons, Mathlib.Meta.Multiset.range_succ', attach_cons, erase_cons_head, cons_subset_cons, singleton_eq_cons_iff, FreeCommRing.of_cons, nodup_iff_le, cons_le_of_notMem, dedup_cons_of_notMem, sub_cons, mem_cons, inf_cons, sym2_cons, cons_sub_of_le, cons_product, lt_cons_self, disjoint_cons_left, erase_cons_tail, join_cons, cons_erase, cons_sigma, subset_cons, count_cons_of_ne, countP_cons_of_neg, disjoint_cons_right, countP_cons_of_pos, count_le_count_cons, powerset_cons, foldl_cons, cons_lt_cons_iff, rel_iff, pmap_cons, erase_le_iff_le_cons, filterMap_cons_some, filterMap_cons, sum_cons, powersetAux'_cons, filter_cons_of_pos, bind_cons, Nat.antidiagonal_succ_succ', le_cons_self, rel_cons_right, erase_cons_tail_of_mem, foldr_cons, Sym.coe_cons, exists_multiset_prod_cons_le_and_prod_not_le, dedup_cons_of_mem, esymm_pair_two, cons_coe, mem_cons_self, Ioo_cons_left, Nodup.cons, cons_inj_left, cons_inj_right, consEquiv_symm_none, covBy_cons, cons_inter_of_neg, range_succ, count_cons_self, le_cons_of_notMem, cons_ndinter_of_mem, insert_eq_cons, filter_cons_of_neg, fold_cons'_right, Ico_cons_right, cons_le_cons, cons_bind, cons_inter_distrib, esymm_pair_one, cons_zero, cons_le_cons_iff, fold_cons_right, gcd_cons, coe_consEquiv_of_ne, keys_cons, filterMap_cons_none, cons_lt_cons, powersetCardAux_cons, Mathlib.Meta.Multiset.insert_eq_cons, map_eq_cons
|
inhabitedMultiset 📖 | CompOp | — |
instEmptyCollection 📖 | CompOp | 10 mathmath: Ico_filter_lt_of_le_left, filter_singleton, Fin.cycleType_cycleIcc_of_ge, Ico_filter_le_of_right_le, alternatingGroup.mem_kleinFour_of_order_two_pow, empty_eq_zero, instLawfulSingleton, Polynomial.roots_one, instIsEmptyToTypeEmptyCollection, Polynomial.roots_def
|
instInsert 📖 | CompOp | 27 mathmath: ADEInequality.sumInv_pqr, Relation.cutExpand_double_left, Polynomial.aroots_quadratic_eq_pair_iff_of_ne_zero', card_eq_three, Relation.cutExpand_double, Equiv.Perm.cycleType_swap_mul_swap_of_nodup, Polynomial.nthRoots_two_one, Polynomial.roots_quadratic_eq_pair_iff_of_ne_zero, alternatingGroup.coe_kleinFour_of_card_eq_four, alternatingGroup.mem_kleinFour_of_order_two_pow, sum_pair, card_eq_four, Cubic.splits_iff_roots_eq_three, Relation.cutExpand_pair_left, alternatingGroup.coe_two_sylow_of_card_eq_four, instLawfulSingleton, Polynomial.aroots_quadratic_eq_pair_iff_of_ne_zero, pair_comm, Relation.cutExpand_pair_right, card_eq_two, Polynomial.roots_quadratic_eq_pair_iff_of_ne_zero', card_pair, prod_pair, insert_eq_cons, Equiv.Perm.closure_cycleType_eq_2_2_eq_alternatingGroup, ADEInequality.classification, Mathlib.Meta.Multiset.insert_eq_cons
|
instOrderBot 📖 | CompOp | 50 mathmath: disjoint_finset_sum_left, UniqueFactorizationMonoid.disjoint_normalizedFactors, isAtom_singleton, disjoint_add_left, range_disjoint_map_add, disjoint_singleton, MvPolynomial.degrees_def, sup_powerset_len, add_eq_union_iff_disjoint, disjoint_list_sum_left, disjoint_union_left, finset_sum_eq_sup_iff_disjoint, nodup_bind, disjoint_finset_sum_right, bot_eq_zero, disjoint_sum_left, nodup_sup_iff, disjoint_map_map, MvPolynomial.degrees_sum_le, Nodup.add_iff, pairwise_disjoint_powersetCard, map_finset_sup, disjoint_left, mem_sup, disjoint_toFinset, Ico_disjoint_Ico, disjoint_cons_left, count_finset_sup, disjoint_union_right, Finset.disjoint_val, disjoint_cons_right, zero_disjoint, disjoint_ndinsert_right, coe_disjoint, card_Iic, disjoint_right, disjoint_of_nodup_add, Finset.sup_toFinset, disjoint_add_right, add_eq_union_left_of_le, ndinter_eq_zero_iff_disjoint, add_eq_union_right_of_le, disjoint_list_sum_right, isAtom_iff, disjoint_ndinsert_left, disjoint_sum_right, singleton_disjoint, disjoint_iff_ne, inter_eq_zero_iff_disjoint, nodup_add
|
instSingleton 📖 | CompOp | 164 mathmath: Nat.Partition.indiscrete_parts, powersetCard_zero_left, le_singleton, ADEInequality.sumInv_pqr, Polynomial.aroots_X_sub_C, Nat.antidiagonalTuple_one, singleton_add, Polynomial.roots_monomial, Nat.antidiagonalTuple_zero_right, singleton_join, Relation.cutExpand_double_left, Polynomial.roots_C_mul_X_pow, Polynomial.aroots_quadratic_eq_pair_iff_of_ne_zero', filter_cons, Finset.singleton_val, product_singleton, sigma_singleton, filter_singleton, powersetCard_one, Polynomial.aroots_X, card_eq_three, map_singleton, prime_factors_irreducible, isAtom_singleton, Polynomial.roots_degree_eq_one, UniqueFactorizationMonoid.factors_eq_singleton_of_irreducible, disjoint_singleton, Nat.antidiagonal_zero, Relation.cutExpand_double, lcm_singleton, addHom_ext_iff, Equiv.Perm.cycleType_swap_mul_swap_of_nodup, sup_singleton, singleton_inj, Sym.coe_equivNatSumOfFintype_symm_apply, Finsupp.toMultiset_apply, Polynomial.roots_X_pow_char_pow_sub_C_pow, Polynomial.nthRoots_two_one, nsmul_cons, AlternatingGroup.card_of_cycleType_singleton, Acc.cutExpand, bind_singleton, powerset_zero, keys_singleton, Equiv.Perm.cycleType_of_card_le_mem_cycleType_add_two, count_singleton_self, Ico_filter_le_left, Polynomial.roots_C_mul_X_sub_C_of_IsUnit, ndinsert_zero, Polynomial.roots_quadratic_eq_pair_iff_of_ne_zero, Relation.cutExpand_singleton, prod_singleton, Relation.cutExpand_zero, Polynomial.roots_C_mul_X_add_C, alternatingGroup.coe_kleinFour_of_card_eq_four, Relation.cutExpand_single_add, gcd_singleton, alternatingGroup.mem_kleinFour_of_order_two_pow, sum_pair, MvPolynomial.degrees_X, singleton_bind, card_eq_four, Polynomial.roots_X_sub_C, Equiv.Perm.IsCycle.cycleType, Nat.Partition.partition_one_parts, sections_zero, ssubset_singleton_iff, map_single_le_powerset, Polynomial.roots_X, Cubic.splits_iff_roots_eq_three, Relation.cutExpand_pair_left, card_singleton, MvPolynomial.degrees_indicator, SimpleGraph.Walk.coe_support_append, filterMap_eq_bind, Polynomial.roots_X_pow_char_sub_C_pow, sum_singleton, toFinsupp_singleton, singleton_eq_cons_iff, Relation.cutExpand_singleton_singleton, Equiv.Perm.IsThreeCycle.cycleType, antidiagonal_zero, alternatingGroup.coe_two_sylow_of_card_eq_four, singleton_subset, erase_singleton, mem_singleton, instLawfulSingleton, Polynomial.aroots_quadratic_eq_pair_iff_of_ne_zero, pair_comm, coe_eq_singleton, Icc_self, List.cycleType_formPerm, toFinset_card_eq_one_iff, UniqueFactorizationMonoid.normalizedFactors_irreducible, Relation.cutExpand_pair_right, Polynomial.aroots_C_mul_X_pow, card_eq_two, replicate_subset_singleton, cycleType_finRotate, sub_singleton, toList_eq_singleton_iff, Polynomial.aroots_monomial, Finset.sum_multiset_singleton, Polynomial.aroots_X_pow, cycleType_finRotate_of_le, Polynomial.roots_C_mul_X_sub_C, filterMap_cons, sum_map_singleton, BoxIntegral.TaggedPrepartition.single_boxes_val, toDFinsupp_singleton, Polynomial.roots_quadratic_eq_pair_iff_of_ne_zero', nsmul_singleton, Equiv.Perm.isSwap_iff_cycleType, mem_singleton_self, Polynomial.roots_X_pow_char_sub_C, Sym.oneEquiv_apply, card_eq_one, fold_singleton, PrimeMultiset.coePNat_ofPrime, MvPolynomial.degrees_X', sort_singleton, count_singleton, inf_singleton, filter_eq_bind, esymm_pair_two, lt_singleton, Finsupp.toMultiset_single, Cycle.lists_nil, coe_singleton, add_singleton_eq_iff, Polynomial.roots_X_pow, singleton_le, Polynomial.roots_X_add_C, card_pair, prod_pair, Equiv.Perm.card_of_cycleType_singleton, Fin.cycleType_cycleIcc_of_lt, toFinset_sum_count_nsmul_eq, toList_singleton, pure_def, Associates.factors_self, Equiv.Perm.closure_cycleType_eq_2_2_eq_alternatingGroup, esymm_pair_one, nodup_singleton, Fin.cycleType_cycleRange, cons_zero, Polynomial.roots_C_mul_X_add_C_of_IsUnit, PrimeMultiset.coeNat_ofPrime, dedup_singleton, replicate_one, foldr_singleton, pi_zero, map_eq_singleton, isAtom_iff, toFinset_singleton, Nat.antidiagonalTuple_zero_zero, singleton_disjoint, SimpleGraph.Walk.coe_support_append', ADEInequality.classification, Relation.cutExpand_add_single, SimpleGraph.Walk.coe_support, Polynomial.roots_X_pow_char_pow_sub_C, Finset.val_eq_singleton_iff, toFinset_eq_singleton_iff
|
instUniqueOfIsEmpty 📖 | CompOp | — |
instZero 📖 | CompOp | 172 mathmath: Cycle.toMultiset_eq_nil, Sym.toMultiset_zero, prod_zero, UniqueFactorizationMonoid.factors_one, IsAlgClosed.roots_eq_zero_iff_degree_nonpos, add_zero, card_eq_zero, zero_product, powersetCard_zero_left, le_singleton, join_zero, dedup_eq_zero, notMem_zero, zero_ndunion, Finsupp.toMultiset_zero, Polynomial.irreducible_iff_roots_eq_zero_of_degree_le_three, sup_zero, powersetCard_zero_right, Ico_eq_zero, filter_cons, powersetCard_card_add, coe_eq_zero, map_eq_zero, Polynomial.roots_eq_zero_iff_isRoot_eq_bot, toFinset_eq_empty, keys_zero, bind_filterMap, Ioc_eq_zero, bind_zero, Polynomial.roots_zero, UniqueFactorizationMonoid.normalizedFactors_zero, Icc_eq_zero_iff, recOn_0, Polynomial.roots_eq_zero_of_irreducible_of_natDegree_ne_one, eq_zero_iff_forall_notMem, IsSepClosed.roots_eq_zero_iff, bind_filter, bell_zero, Cycle.nil_toMultiset, disjoint_list_sum_left, Mathlib.Meta.Multiset.range_zero', map_zero, Associates.count_zero, powerset_zero, MvPolynomial.degrees_C, UniqueFactorizationMonoid.normalizedFactors_one, UniqueFactorizationMonoid.normalizedFactors_pos, inf_zero, Finset.val_eq_zero, ndinsert_zero, UniqueFactorizationMonoid.factors_pos, dedup_zero, not_nodup_pair, Relation.cutExpand_zero, sym2_eq_zero_iff, filter_eq_nil, lcm_zero, Nat.Partition.partition_zero_parts, sections_zero, sort_zero, ssubset_singleton_iff, disjSum_zero, product_zero, UniqueFactorizationMonoid.normalizedFactors_of_isUnit, bot_eq_zero, filterMap_zero, sum_zero, multinomial_zero, IsAlgClosed.roots_eq_zero_iff_natDegree_eq_zero, fold_zero, filterMap_eq_bind, Ioc_eq_zero_of_le, count_zero, empty_toList, empty_eq_zero, MvPolynomial.degreesLE_zero, foldl_zero, zero_add, sym2_zero, singleton_eq_cons_iff, nodup_iff_le, MvPolynomial.degrees_one, Polynomial.aroots_zero, inter_zero, Ioo_self, card_zero, Polynomial.nthRoots_zero, antidiagonal_zero, Icc_eq_zero_of_lt, toFinset_zero, Ioo_eq_zero_iff, Ico_eq_zero_of_le, zero_subset, zero_ndinter, Equiv.Perm.cycleType_eq_zero, erase_singleton, powersetCard_eq_empty, Finset.mk_zero, toFinsupp_zero, zero_sub, Ico_inter_Ico_of_le, Equiv.Perm.cycleType_one, subset_zero, Polynomial.nthRoots_two_eq_zero_iff, Ioo_eq_zero, zero_inter, rel_iff, zero_disjoint, Sym.coe_nil, powersetAux'_nil, erase_zero, le_zero, MvPolynomial.degrees_zero, foldr_zero, filterMap_cons, zero_union, pmap_zero, gcd_zero, UniqueFactorizationMonoid.normalizedFactors_eq_zero_iff, Polynomial.aroots_one, IsAlgClosed.roots_eq_zero_iff, attach_zero, Polynomial.roots_eq_zero_iff_eq_zero_or_isRoot_eq_bot, filter_false, replicate_zero, Finset.empty_val, filter_eq_bind, Ico_eq_zero_iff, lt_singleton, zero_sigma, filter_zero, Polynomial.exists_prod_multiset_X_sub_C_mul, rel_zero_right, UniqueFactorizationMonoid.factors_zero, Nat.antidiagonalTuple_zero_succ, Disjoint.ndinter_eq_zero, range_zero, instIsEmptyToTypeOfNat, Icc_eq_zero, zero_le, union_zero, eq_zero_of_forall_notMem, toList_eq_nil, countP_zero, zero_bind, Ioc_eq_zero_iff, cons_zero, UniqueFactorizationMonoid.factors_of_isUnit, ndinter_eq_zero_iff_disjoint, Ioc_self, pi_zero, Associates.factors_one, Polynomial.aroots_C, disjoint_list_sum_right, UniqueFactorizationMonoid.factors_eq_zero, Polynomial.roots_C, empty_or_exists_mem, nodup_zero, toList_zero, zero_ssubset, rel_zero_left, Ico_self, Relation.not_cutExpand_zero, powersetCardAux_zero, pairwise_zero, Polynomial.Monic.irreducible_iff_roots_eq_zero_of_degree_le_three, inter_eq_zero_iff_disjoint, sub_zero, Ioo_eq_zero_of_le, zero_disjSum, coe_nil, coe_eq_zero_iff_isEmpty
|
rec 📖 | CompOp | — |
recOn 📖 | CompOp | — |
zero 📖 | CompOp | — |
«term_::ₘ_» 📖 | CompOp | — |