prod 📖 | CompOp | 320 mathmath: prod_zero, Polynomial.splits_iff_exists_multiset, ofAdd_multiset_prod, Polynomial.eval_multiset_prod, Set.multiset_prod_subset_multiset_prod, prod_replicate, prod_int_mod, Polynomial.eval₂_multiset_prod, prod_induction, aestronglyMeasurable_fun_prod, Finset.prod_multiset_map_count, Polynomial.leadingCoeff_multiset_prod', Height.mulHeight₁_eq, hasFDerivAt_multiset_prod, Asymptotics.IsEquivalent.multisetProd, Polynomial.mahlerMeasure_eq_leadingCoeff_mul_prod_roots, Nat.coprime_multiset_prod_right_iff, IsNonarchimedean.multiset_powerset_image_add, ArithmeticFunction.cardFactors_multiset_prod, prod_X_sub_X_eq_sum_esymm, prod_map_neg, Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq, Equiv.Perm.card_of_cycleType_mul_eq, Subfield.multiset_prod_mem, fderiv_multiset_prod, Associates.prod_le_prod, prod_eq_pow_single, Nat.factors_multiset_prod_of_irreducible, Polynomial.monic_multisetProd_X_sub_C, prod_map_sum, prod_join, noncommProd_eq_prod, Finsupp.prod_toMultiset, Polynomial.one_le_prod_max_one_norm_roots, stronglyMeasurable_fun_prod, Polynomial.Splits.eval_derivative, card_pi, one_le_prod_of_one_le, UniqueFactorizationMonoid.exists_prime_factors, prod_bind, prod_eq_zero, prod_sum, Polynomial.eq_prod_roots_of_splits, Polynomial.eq_prod_roots_of_monic_of_splits_id, prod_normalizedFactors_eq_self, Polynomial.map_sub_roots_sprod_eq_prod_map_eval, prod_map_pow, prod_X_add_C_coeff, Polynomial.Splits.eval_root_derivative, IsUltrametricDist.exists_norm_multiset_prod_le, Equiv.Perm.OnCycleFactors.kerParam_range_card, tendsto_multiset_prod, HasFDerivWithinAt.multiset_prod, multiset_prod_mem, Int.ModEq.multisetProd_one, CanonicallyOrderedAdd.multiset_prod_pos, Finset.prod_multiset_count_of_subset, prod_dvd_prod_of_le, Polynomial.Splits.multisetProd, Associates.prod_le_prod_iff_le, Real.multiset_prod_map_rpow, hasStrictFDerivAt_multiset_prod, toAdd_multiset_sum, prod_cons, Polynomial.prod_roots_eq_coeff_zero_of_monic_of_splits, Nat.ModEq.multisetProd_map, Polynomial.monic_multiset_prod_of_monic, Polynomial.eval_derivative_of_splits, prod_X_sub_C_dvd_iff_le_roots, Polynomial.leadingCoeff_mul_prod_normalizedFactors, ofMul_multiset_prod, prod_nonneg, aemeasurable_prod, Polynomial.prod_multiset_root_eq_finset_root, MulHom.map_multiset_ne_zero_prod, NNRat.cast_multisetProd, IsMulFreimanIso.map_prod_eq_map_prod, smul_prod', prod_lt_prod', le_prod_of_submultiplicative_on_pred_of_nonneg, Ideal.IsPrime.multiset_prod_map_le, Polynomial.Splits.coeff_zero_eq_prod_roots_of_monic, Polynomial.prod_multiset_X_sub_C_dvd, NNReal.coe_multiset_prod, Polynomial.coeff_zero_eq_leadingCoeff_mul_prod_roots_of_splits, Finset.prod_val, Polynomial.resultant_eq_prod_eval, AddMonoidAlgebra.sup_support_multiset_prod_le, Pi.multiset_prod_apply, measurable_prod, IntermediateField.multiset_prod_mem, prod_map_lt_prod_map, prod_map_erase, prod_eq_zero_iff, bell_mul_eq, Polynomial.evalEval_multiset_prod, prod_map_le_prod, UniqueFactorizationMonoid.normalizedFactors_prod_of_prime, Subalgebra.multiset_prod_mem, Ideal.multiset_prod_span_singleton, Subring.multiset_prod_mem, prod_hom_rel, mem_le_prod_of_one_le, aemeasurable_fun_prod, prod_singleton, Asymptotics.IsLittleO.multisetProd, Equiv.Perm.card_isConj_eq, Polynomial.multiset_prod_comp, prod_toList, prod_filter_mul_prod_filter_not, MvPolynomial.totalDegree_multiset_prod, Polynomial.Splits.eq_prod_roots, spectralNorm.spectralNorm_pow_natDegree_eq_prod_roots, prod_map_add, toFinset_prod_dvd_prod, Subgroup.multiset_prod_mem, Polynomial.prod_max_one_norm_roots_le_mahlerMeasure_of_one_le_leadingCoeff, norm_multiset_prod_le, prod_nat_mod, gal_prod_isSolvable, Int.cast_multiset_prod, prod_map_nonneg, Polynomial.Splits.aeval_eq_prod_aroots, Set.image_multiset_prod, Equiv.Perm.card_of_cycleType, WfDvdMonoid.not_unit_iff_exists_factors_eq, Matrix.det_eq_prod_roots_charpoly_of_splits, apply_prod_le_sum_map, untrop_prod, prod_map_mul, IsIntegral.multiset_prod, prod_eq_prod_toEnumFinset, Polynomial.map_sub_sprod_roots_eq_prod_map_eval, prod_eq_prod_coe, pow_card_le_prod, Polynomial.degree_multiset_prod_of_monic, le_prod_of_submultiplicative_of_nonneg, Polynomial.Splits.eval_eq_prod_roots_of_monic, le_prod_of_mem, Associates.prod_mk, dvd_prod, periodic_prod, Rat.cast_multiset_prod, Nat.chineseRemainderOfMultiset_lt_prod, trop_sum, prod_lt_prod_of_nonempty', Ideal.IsPrime.multiset_prod_le, HasFDerivAt.multiset_prod, Nat.coprime_multiset_prod_left_iff, Polynomial.prod_mahlerMeasure_eq_mahlerMeasure_prod, Polynomial.eq_prod_roots_of_splits_id, Finset.prod_mk, AlternatingGroup.card_of_cycleType, Polynomial.eval_eq_prod_roots_sub_of_splits_id, Polynomial.natDegree_multiset_prod, prod_map_inv', Height.mulHeight_eq, prod_nsmul, Polynomial.aeval_eq_prod_aroots_sub_of_monic_of_splits, prod_map_product_eq_prod_prod, sum_map_le_apply_prod, Asymptotics.IsTheta.multisetProd, Nat.sum_divisors_filter_squarefree, Polynomial.roots_multiset_prod_X_sub_C, PrimeSpectrum.exists_primeSpectrum_prod_le, continuous_multiset_prod, prod_map_le_pow_card, Submonoid.exists_multiset_of_mem_closure, Polynomial.Splits.eval_eq_prod_roots, prod_map_le_prod_map₀, prod_map_prod, map_multiset_prod, Asymptotics.IsBigO.multisetProd, Ideal.IsPrime.multiset_prod_mem_iff_exists_mem, fderivWithin_multiset_prod, prod_induction_nonempty, Finset.prod_map_val, Polynomial.natDegree_multiset_prod_X_sub_C_eq_card, Nat.ModEq.multisetProd_map_one, prod_map_zpow, one_le_prod, Real.exp_multiset_sum, UniqueFactorizationMonoid.factors_prod, Polynomial.Monic.nextCoeff_multiset_prod, Polynomial.ofMultiset_apply, Polynomial.eval_eq_prod_roots_sub_of_monic_of_splits_id, prod_le_prod_of_rel_le, Polynomial.multiset_prod_X_sub_C_nextCoeff, Nat.cast_multiset_prod, Polynomial.aeval_derivative_of_splits, Polynomial.derivative_prod, PrincipalIdealRing.factors_spec, PrimeMultiset.prod_ofPNatMultiset, prod_map_le_prod_map, Polynomial.degree_multiset_prod_le, nat_divisors_prod, Polynomial.coeff_zero_multiset_prod, pow_count, bell_eq, Set.multiset_prod_singleton, Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C, max_prod_le, IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots, continuousOn_multiset_prod, prod_map_div, UniqueFactorizationMonoid.prod_normalizedFactors, Polynomial.Splits.aeval_eq_prod_aroots_of_monic, Polynomial.Splits.eq_prod_roots_of_monic, Submonoid.multiset_prod_mem, Polynomial.resultant_eq_prod_roots_sub, Polynomial.aeval_eq_prod_aroots_sub_of_splits, UniqueFactorizationMonoid.normalizedFactors_prod_eq, le_prod_nonempty_of_submultiplicative_on_pred, UniqueFactorizationMonoid.iff_exists_prime_factors, prod_hom, Polynomial.aeval_root_derivative_of_splits, prod_eq_one_iff, prod_map_eq_pow_single, Finset.prod_eq_multiset_prod, prod_add, TwoSidedIdeal.multiSetProd_mem, nnnorm_multiset_prod_le, map_multiset_ne_zero_prod, Real.log_multiset_prod, Polynomial.Splits.coeff_zero_eq_leadingCoeff_mul_prod_roots, multisetProd_apply_eq_zero', prod_erase, HasStrictFDerivAt.multiset_prod, Int.ModEq.multisetProd_map_one, Matrix.det_eq_prod_roots_charpoly, toMul_multiset_sum, Algebra.norm_eq_prod_roots, Polynomial.eval₂_derivative_of_splits, multisetProd_apply_eq_zero, prod_le_prod_map, Polynomial.leadingCoeff_multiset_prod, prod_dvd_prod_of_dvd, one_le_prod_map, card_sections, prod_map_prod_map, exists_multiset_prod_cons_le_and_prod_not_le, RingEquiv.map_multiset_prod, le_prod_of_submultiplicative_on_pred, Ideal.multiset_prod_le_inf, MonoidHom.map_multiset_prod, prod_X_add_C_eq_sum_esymm, Polynomial.exists_prod_multiset_X_sub_C_mul, Algebra.PowerBasis.norm_gen_eq_prod_roots, Polynomial.natDegree_multiset_prod', Polynomial.splits_iff_exists_multiset', PrimeMultiset.prod_ofNatMultiset, prod_X_add_C_coeff', UniqueFactorizationMonoid.prod_normalizedFactors_eq, Polynomial.splits_of_exists_multiset, le_prod_of_submultiplicative, NumberField.prod_archAbsVal_eq, sup_eq_prod_inf_factors, snd_prod, Subsemiring.multiset_prod_mem, Polynomial.natDegree_multiset_prod_le, Ideal.multiset_prod_eq_bot, Submonoid.coe_multiset_prod, Polynomial.map_multiset_prod, Nat.divisors_filter_squarefree, Finset.sum_pow, aestronglyMeasurable_prod, Polynomial.roots_multiset_prod, Polynomial.degree_multiset_prod, WfDvdMonoid.exists_factors, Polynomial.multiset_prod_X_sub_C_coeff_card_pred, AddMonoidAlgebra.le_inf_support_multiset_prod, prod_pair, Associates.prod_eq_one_iff, Differential.logDeriv_multisetProd, stronglyMeasurable_prod, prod_eq_one, prod_coe, prod_hom₂_ne_zero, Set.multiset_prod_mem_multiset_prod, smul_prod, Equiv.Perm.sign_of_cycleType', Con.multiset_prod, Height.AdmissibleAbsValues.product_formula, Finset.prod_multiset_count, Polynomial.natDegree_multiset_prod_of_monic, le_prod_nonempty_of_submultiplicative, NNReal.multiset_prod_map_rpow, prod_primes_dvd, Int.ModEq.multisetProd_map, prod_le_pow_card, single_le_prod, enorm_multisetProd_le, Polynomial.coeff_multiset_prod_of_natDegree_le, Complex.exp_multiset_sum, prod_pos, prod_hom_ne_zero, prod_map_toList, PrimeSpectrum.exists_primeSpectrum_prod_le_and_ne_bot_of_domain, prod_hom₂, SubmonoidClass.coe_multiset_prod, prod_eq_foldr, prod_map_one, PrimeMultiset.coe_prod, AlternatingGroup.card_of_cycleType_mul_eq, Associates.prod_coe, measurable_fun_prod, Equiv.Perm.card_isConj_mul_eq, UniqueFactorizationMonoid.normalizedFactors_multiset_prod, Equiv.Perm.nat_card_centralizer, prod_eq_foldl, prod_map_inv, Subgroup.val_multiset_prod, Nat.ModEq.multisetProd_one, Polynomial.eval_multiset_prod_X_sub_C_derivative, Ideal.sup_multiset_prod_eq_top, prod_min_le, Polynomial.coeff_zero_eq_prod_roots_of_monic_of_splits, prod_hom', fst_prod, prod_X_sub_C_coeff
|
sum 📖 | CompOp | 262 mathmath: Finsupp.sum_toMultiset, IntermediateField.AdjoinSimple.trace_gen_eq_sum_roots, ofAdd_multiset_prod, Nat.Partition.ofMultiset_parts, map_multiset_sum, Ideal.pow_multiset_sum_mem_span_pow, sum_induction, convexHull_multiset_sum, Int.ModEq.multisetSum_map_zero, hasFDerivAt_multiset_prod, IsNonarchimedean.multiset_powerset_image_add, ArithmeticFunction.cardFactors_multiset_prod, sum_eq_foldr, Equiv.Perm.sign_of_cycleType, Finsupp.multiset_sum_sum_index, Equiv.Perm.card_of_cycleType_mul_eq, sum_map_le_sum, fderiv_multiset_prod, WithLp.ofLp_multisetSum, prod_map_sum, Polynomial.Splits.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff, aemeasurable_sum, Polynomial.Splits.eval_derivative, sum_eq_sum_toEnumFinset, sum_map_zsmul, vadd_sum, Equiv.Perm.OnCycleFactors.kerParam_range_card, coe_sumAddMonoidHom, sum_eq_nsmul_single, Nat.cast_multiset_sum, sum_smul_sum, CharTwo.multiset_sum_sq, smul_sum, Matrix.trace_multiset_sum, norm_multiset_sum_le, HasFDerivWithinAt.multiset_prod, support_sum_subset, Polynomial.Splits.eval_derivative_eq_eval_mul_sum, Nat.ModEq.multisetSum_map_zero, Int.cast_multiset_sum, sum_add, untrop_sum, sum_map_neg, sum_le_sum_map, hasStrictFDerivAt_multiset_prod, toAdd_multiset_sum, sum_le_card_nsmul, Polynomial.eval_derivative_of_splits, AddSubmonoidClass.coe_multiset_sum, ofMul_multiset_prod, sum_nat_mod, WithLp.toLp_multisetSum, continuous_multiset_sum, multiset_sum_pow_char_pow, count_sum, IsIntegral.multiset_sum, Equiv.Perm.card_of_cycleType_eq_zero_iff, IsNonarchimedean.multiset_image_add_of_nonempty, card_nsmul_le_sum, periodic_sum, Finset.sum_val, AddSubgroup.multiset_sum_mem, AddMonoidAlgebra.sup_support_multiset_prod_le, Subalgebra.multiset_sum_mem, multiset_sum_pow_char, Pi.multiset_sum_apply, bell_mul_eq, Finset.sum_mk, nnnorm_multiset_sum_le, sum_le_sum_of_rel_le, nsmul_count, sum_erase, sum_hom₂, Nat.ModEq.multisetSum_map, Equiv.Perm.card_isConj_eq, IsUltrametricDist.exists_norm_multiset_sum_le, MvPolynomial.totalDegree_multiset_prod, Polynomial.eval_derivative_eq_eval_mul_sum_of_splits, sum_hom_ne_zero, prod_map_add, sum_map_tsub, Polynomial.Splits.eval_derivative_div_eval_of_ne_zero, sum_nsmul, max_sum_le, norm_multiset_prod_le, sum_pair, le_sum_nonempty_of_subadditive_on_pred, Equiv.Perm.card_of_cycleType, Matrix.transpose_multiset_sum, sum_coe, Set.multiset_sum_mem_multiset_sum, sum_eq_foldl, Matrix.diag_multiset_sum, apply_prod_le_sum_map, sum_induction_nonempty, untrop_prod, stronglyMeasurable_sum, snd_sum, sum_hom_rel, trop_inf, sum_map_erase, Matrix.trace_eq_sum_roots_charpoly, Polynomial.degree_multiset_prod_of_monic, Polynomial.logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots, Commute.multiset_sum_right, sum_sum, sum_filter_add_sum_filter_not, trop_sum, disjoint_sum_left, AddCon.multiset_sum, HasFDerivAt.multiset_prod, Int.ModEq.multisetSum_map, Polynomial.Splits.nextCoeff_eq_neg_sum_roots_of_monic, sum_zero, TwoSidedIdeal.multisetSum_mem, trace_eq_sum_roots, AlternatingGroup.card_of_cycleType, Equiv.Perm.sum_cycleType_le, Polynomial.natDegree_multiset_prod, Matrix.trace_eq_sum_roots_charpoly_of_splits, sum_map_eq_nsmul_single, Subfield.multiset_sum_mem, AddSubmonoid.exists_multiset_of_mem_closure, aestronglyMeasurable_sum, Equiv.Perm.centralizer_le_alternating_iff, tendsto_multiset_sum, sum_smul, sum_singleton, TensorProduct.exists_multiset, sum_map_le_apply_prod, Equiv.Perm.card_fixedPoints, Polynomial.eval_derivative_div_eval_of_ne_zero_of_splits, Set.image_multiset_sum, Int.ModEq.multisetSum_zero, Finset.sum_eq_multiset_sum, fst_sum, fderivWithin_multiset_prod, NNRat.cast_multisetSum, sum_map_div, sum_replicate, count_bind, multiset_sum_mem, sum_map_zero, Real.exp_multiset_sum, sum_map_neg', Polynomial.Monic.nextCoeff_multiset_prod, Commute.multiset_sum_left, CharTwo.multiset_sum_mul_self, Polynomial.multiset_prod_X_sub_C_nextCoeff, LinearMap.BilinMap.toQuadraticMap_multiset_sum, Polynomial.aeval_derivative_of_splits, Polynomial.sum_roots_eq_nextCoeff_of_monic_of_split, sum_toList, Polynomial.derivative_prod, sum_map_le_sum_map, convex_multiset_sum, Polynomial.nextCoeff_eq_neg_sum_roots_of_monic_of_splits, Finset.sum_multiset_map_count, sum_bind, Polynomial.degree_multiset_prod_le, bell_eq, aemeasurable_fun_sum, sum_lt_sum_of_nonempty, sum_nonneg, IntermediateField.multiset_sum_mem, ZMod.erdos_ginzburg_ziv_multiset, sum_hom₂_ne_zero, Finsupp.single_multiset_sum, support_sum_eq, sum_map_sub, RingCon.multisetSum, Finsupp.multiset_sum_sum, PowerBasis.trace_gen_eq_sum_roots, sum_eq_zero, nnnorm_multiset_prod_le, Matrix.conjTranspose_multiset_sum, Real.log_multiset_prod, AddSubmonoid.coe_multiset_sum, AddSubgroup.val_multiset_sum, sum_map_singleton, HasStrictFDerivAt.multiset_prod, sum_cons, NNReal.coe_multiset_sum, Equiv.Perm.card_le_of_centralizer_le_alternating, toMul_multiset_sum, Polynomial.eval₂_derivative_of_splits, sum_lt_sum, map_multiset_ne_zero_sum, RingEquiv.map_multiset_sum, AddMonoidHom.map_multiset_sum, WithConv.toConv_multisetSum, IsAddFreimanIso.map_sum_eq_map_sum, Localization.mk_multiset_sum, Equiv.Perm.exists_with_cycleType_iff, card_join, sum_map_sum, Polynomial.eval₂_multiset_sum, le_sum_of_subadditive_on_pred, le_sum_of_subadditive, IsNonarchimedean.multiset_image_add, Nat.Partition.parts_sum, enorm_multisetSum_le, WithConv.ofConv_multisetSum, sum_min_le, Int.erdos_ginzburg_ziv_multiset, Polynomial.eval_multisetSum, sum_join, Polynomial.natDegree_multiset_prod', sum_eq_sum_coe, stronglyMeasurable_fun_sum, sum_hom, dvd_sum, Set.multiset_sum_singleton, Polynomial.natDegree_multiset_prod_le, Set.multiset_sum_subset_multiset_sum, abs_sum_le_sum_abs, measurable_fun_sum, Equiv.Perm.sum_cycleType, Finset.sum_map_val, Rat.cast_multiset_sum, sum_map_add, Polynomial.degree_multiset_prod, sum_map_mul_right, Polynomial.multiset_prod_X_sub_C_coeff_card_pred, AddMonoidAlgebra.le_inf_support_multiset_prod, Differential.logDeriv_multisetProd, sum_hom', sum_eq_zero_iff, AlternatingGroup.map_subtype_of_cycleType, Subsemiring.multiset_sum_mem, Polynomial.natDegree_multiset_prod_of_monic, Finset.sum_multiset_count, NonUnitalSubring.multiset_sum_mem, card_bind, le_sum_of_mem, enorm_multisetProd_le, Complex.exp_multiset_sum, sum_map_sum_map, le_sum_nonempty_of_subadditive, single_le_sum, sum_map_toList, Finsupp.mapRange_multiset_sum, disjoint_sum_right, AlternatingGroup.card_of_cycleType_mul_eq, continuousOn_multiset_sum, Nat.ModEq.multisetSum_zero, Equiv.Perm.card_isConj_mul_eq, UniqueFactorizationMonoid.normalizedFactors_multiset_prod, Subring.multiset_sum_mem, Equiv.Perm.nat_card_centralizer, sum_map_nsmul, measurable_sum, AddHom.map_multiset_ne_zero_sum, Finset.sum_multiset_count_of_subset, AddSubmonoid.multiset_sum_mem, aestronglyMeasurable_fun_sum, Polynomial.natDegree_multiset_sum_le, card_sigma, sum_int_mod, sum_map_mul_left, noncommSum_eq_sum, Polynomial.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff_of_splits
|