count 📖 | CompOp | 163 mathmath: Equiv.Perm.count_le_one_of_centralizer_le_alternating, Finset.prod_multiset_map_count, Submodule.isInternal_prime_power_torsion_of_pid, cast_symm_apply_fst, le_iff_count, Equiv.Perm.card_of_cycleType_mul_eq, prod_eq_pow_single, sum_count_eq_card, nodup_iff_count_le_one, count_attach, Sym.coe_equivNatSumOfFintype_apply_apply, card_Ico, coe_count, Sym.coe_equivNatSum_apply_apply, sum_toEnumFinset, count_replicate, ext'_iff, toFinset_sum_count_eq, sum_eq_nsmul_single, Polynomial.count_map_roots, PMF.toMeasure_ofMultiset_apply, coe_mem, count_filter_of_pos, toDFinsupp_apply, MvPolynomial.degreeOf_def, Ideal.count_normalizedFactors_eq, Sym.count_coe_fill_self_of_notMem, consEquiv_symm_some, Equiv.Perm.OnCycleFactors.nat_card_range_toPermHom, Finset.prod_multiset_count_of_subset, Finset.map_sym_eq_piAntidiag, coeEmbedding_apply, Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal, UniqueFactorizationMonoid.factors_pow_count_prod, count_eq_card_filter_eq, DividedPowers.dpow_sum', Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count, Finset.sum_count_of_mem_sym, ChevalleyThm.chevalley_mvPolynomialC, Associates.count_some, count_sum, count_singleton_self, card_Ioc, bell_mul_eq, ext, nsmul_count, count_cons, Polynomial.count_map_roots_of_injective, PowerSeries.normalized_count_X_eq_of_coe, toFinsupp_apply, Equiv.Perm.card_isConj_eq, count_le_of_le, UniqueFactorizationMonoid.count_normalizedFactors_eq, PNat.count_factorMultiset, multinomial_filter_ne, card_uIcc, card_le_card_toFinset_add_one_iff, Equiv.Perm.card_of_cycleType, norm_iteratedFDerivWithin_prod_le, PMF.toOuterMeasure_ofMultiset_apply, count_filter_of_neg, DividedPowers.dpow_sum, Polynomial.count_roots, map_count_True_eq_filter_card, prod_eq_prod_coe, replicate_inter, Finsupp.count_toMultiset, map_univ_coe, Polynomial.exists_multiset_roots, count_union, count_span_normalizedFactors_eq_of_normUnit, Sym.count_coe_fill_of_ne, count_pos, AlternatingGroup.card_of_cycleType, cast_apply_fst, filter_eq, count_zero, sum_map_eq_nsmul_single, irreducible_pow_sup, count_sum', Equiv.Perm.centralizer_le_alternating_iff, count_eq_one_of_mem, mem_toEnumFinset, count_dedup, count_nsmul, count_sub, count_le_card, count_injective, coe_mk, NumberField.count_multisetInfinitePlace_eq_mult, count_bind, count_inter, count_le_of_ideal_ge, count_map, nodup_iff_count_eq_one, map_univ, Finset.sum_multiset_map_count, MvPolynomial.mem_restrictDegree_iff_sup, pow_count, bell_eq, norm_iteratedFDeriv_prod_le, count_finset_sup, count_add, count_map_eq_count, count_cons_of_ne, count_eq_of_nodup, mapEquiv_apply, UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors, count_span_normalizedFactors_eq, count_le_count_cons, prod_map_eq_pow_single, prod_toEnumFinset, count_eq_zero_of_notMem, count_filter, map_univ_comp_coe, Submodule.isInternal_prime_power_torsion, count_erase_of_ne, cast_symm_apply_snd, Nat.Partition.count_ofSums_zero, factorization_eq_count, filter_eq', Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count, card_Iic, mem_sub, coe_countAddMonoidHom, IsDedekindDomain.HeightOneSpectrum.maxPowDividing_eq_pow_multiset_count, coeEquiv_symm_apply_fst, le_count_iff_replicate_le, count_erase_self, Ideal.eq_prime_pow_mul_coprime, Nat.Partition.count_ofSums_of_ne_zero, UniqueFactorizationMonoid.count_normalizedFactors_eq', cast_apply_snd, count_singleton, card_Icc, forall_coe, count_associates_factors_eq, Equiv.Perm.CycleType.count_def, count_eq_zero, sum_eq_sum_coe, consEquiv_symm_none, coeEquiv_symm_apply_snd_val, count_cons_self, count_replicate_self, count_eq_card, toFinset_sum_count_nsmul_eq, count_univ, Finset.prod_multiset_count, Polynomial.count_roots_le_one, Finset.sum_multiset_count, card_Ioo, one_le_count_iff_mem, coe_consEquiv_of_ne, IsDedekindDomain.quotientEquivPiFactors_mk, count_map_eq_count', inter_replicate, AlternatingGroup.card_of_cycleType_mul_eq, toEnumFinset_filter_eq, Equiv.Perm.card_isConj_mul_eq, Equiv.Perm.nat_card_centralizer, PMF.ofMultiset_apply, Finset.sum_multiset_count_of_subset, exists_coe
|