instAdd 📖 | CompOp | 161 mathmath: add_zero, product_cons, foldr_add, toFinsupp_add, revzip_powersetAux, equivDFinsupp_symm_apply, add_inter_distrib, Associates.factors_mul, coe_add, singleton_add, lcm_add, join_add, filter_cons, Icc_eq, fold_add, Finset.disjUnion_val, Relation.cutExpand_add_left, Equiv.Perm.Disjoint.cycleType, Finsupp.toMultiset_toFinsupp, sub_le_iff_le_add', toFinsupp_sum_eq, disjoint_add_left, instCanonicallyOrderedAdd, sum_add, card_add, equivDFinsupp_apply, bind_add, add_le_add_iff_right, add_right_inj, add_eq_union_iff_disjoint, disjoint_list_sum_left, instExistsAddOfLE, nsmul_cons, antidiagonal_cons, add_comm, dedup_add, MvPolynomial.degreesLE_add, toFinsupp_union, toFinset_add, UniqueFactorizationMonoid.normalizedFactors_mul, filter_add_filter, union_add_inter, mem_antidiagonal, Disjoint.ndunion_eq, toFinsupp_inter, inf_add, powersetCard_cons, sub_add_eq_sub_sub, toFinsupp_apply, add_sigma, le_add_sub, Sym.coe_fill, Relation.cutExpand_single_add, add_le_add_iff_left, add_assoc, add_sub_cancel, add_cons, mem_add, Associates.prod_add, sub_add_cancel, instAddLeftMono, uIcc_eq, le_add_left, cons_add, rel_add_left, erase_add_right_pos, Relation.cutExpand_fibration, Relation.cutExpand_le_invImage_lex, filter_add_not, erase_add_left_pos, SimpleGraph.Walk.coe_support_append, replicate_add, zero_add, sub_le_iff_le_add, Finsupp.toMultiset_add, toFinsupp_singleton, Nodup.add_iff, toFinsupp_symm_apply, erase_add_left_neg, add_sub_assoc, Equiv.Perm.OnCycleFactors.cycleType_kerParam_apply_apply, Finsupp.coe_orderIsoMultiset_symm, ndunion_le_add, sym2_cons, add_bind, Ico_add_Ico_eq_Ico, cons_product, Disjoint.dedup_add, erase_add_right_neg, filterMap_add, toFinsupp_zero, gcd_add, MvPolynomial.degrees_mul_le, toFinsupp_toMultiset, rel_add_right, join_cons, Polynomial.roots_mul, Rel.add, count_add, Nat.factorization_eq_primeFactorsList_multiset, revzip_powersetAux', cons_sigma, MvPolynomial.degrees_mul_eq, product_add, toFinsupp_eq_iff, subset_add_left, powerset_cons, prod_add, union_le_add, add_le_add_right, add_product, range_add, filter_add, subset_add_right, filterMap_cons, add_union_distrib, Associates.FactorSet.coe_add, bind_cons, Relation.cutExpand_iff, Relation.cutExpand_add_right, sections_add, instOrderedSub, sub_add_inter, Equiv.Perm.Disjoint.cycleType_mul, le_sub_add, Polynomial.aroots_mul, countP_add, Equiv.Perm.parts_partition, le_add_right, add_le_add_left, map_disjSum, add_sub_cancel_right, Subset.dedup_add_right, union_add_distrib, add_singleton_eq_iff, UniqueFactorizationMonoid.factors_mul, disjoint_add_right, add_left_inj, map_add, Subset.dedup_add_left, le_iff_exists_add, cons_bind, Sym.coe_append, Nat.Partition.coeff_genFun, add_eq_union_left_of_le, add_eq_union_right_of_le, disjoint_list_sum_right, Associates.FactorSet.sup_add_inf_eq_add, foldl_add, toFinsupp_support, toFinsupp_strictMono, instAddLeftReflectLE, sup_add, SimpleGraph.Walk.coe_support_append', inter_add_distrib, union_def, Relation.cutExpand_add_single, nodup_add, SimpleGraph.Walk.coe_support, Finsupp.toMultiset_eq_iff, sigma_add
|