| Metric | Count |
|---|
Definitionsfinprod, finsum, Β«termβαΆ _,_Β», Β«termβαΆ _,_Β» | 4 |
Theoremsmap_finsum, map_finsum_mem, map_finsum, map_finsum, map_finsum_Prop, map_finsum_mem, map_finsum_mem', map_finsum_of_injective, map_finsum_of_preimage_zero, map_finsum_plift, mulSupport_of_fiberwise_prod_subset_image, support_of_fiberwise_sum_subset_image, map_finprod, map_finprod_Prop, map_finprod_mem, map_finprod_mem', map_finprod_of_injective, map_finprod_of_preimage_one, map_finprod_plift, map_finprod, map_finprod_mem, map_finprod, cast_finprod, cast_finprod_mem, cast_finsum, cast_finsum_mem, add_finsum_cond_ne, exists_ne_one_of_finprod_mem_ne_one, exists_ne_zero_of_finsum_mem_ne_zero, finite_mulSupport_of_finprod_ne_one, finite_support_of_finsum_eq_one, finite_support_of_finsum_ne_zero, finprod_apply, finprod_apply_ne_one, finprod_comp, finprod_comp_equiv, finprod_cond_eq_left, finprod_cond_eq_prod_of_cond_iff, finprod_cond_eq_right, finprod_cond_ne, finprod_cond_nonneg, finprod_cond_pos, finprod_congr, finprod_congr_Prop, finprod_curry, finprod_curryβ, finprod_def, finprod_def', finprod_div_distrib, finprod_dmem, finprod_emb_domain, finprod_emb_domain', finprod_eq_dif, finprod_eq_finset_prod_of_mulSupport_subset, finprod_eq_if, finprod_eq_mulIndicator_apply, finprod_eq_of_bijective, finprod_eq_one_of_forall_eq_one, finprod_eq_prod, finprod_eq_prod_of_fintype, finprod_eq_prod_of_mulSupport_subset, finprod_eq_prod_of_mulSupport_subset_of_finite, finprod_eq_prod_of_mulSupport_toFinset_subset, finprod_eq_prod_plift_of_mulSupport_subset, finprod_eq_prod_plift_of_mulSupport_toFinset_subset, finprod_eq_single, finprod_eq_zero, finprod_false, finprod_induction, finprod_inv_distrib, finprod_le_finprod, finprod_le_finprod', finprod_mem_biUnion, finprod_mem_coe_finset, finprod_mem_comm, finprod_mem_congr, finprod_mem_def, finprod_mem_div_distrib, finprod_mem_dvd, finprod_mem_empty, finprod_mem_eq_finite_toFinset_prod, finprod_mem_eq_of_bijOn, finprod_mem_eq_one_of_forall_eq_one, finprod_mem_eq_one_of_infinite, finprod_mem_eq_prod, finprod_mem_eq_prod_filter, finprod_mem_eq_prod_of_inter_mulSupport_eq, finprod_mem_eq_prod_of_subset, finprod_mem_eq_toFinset_prod, finprod_mem_finset_eq_prod, finprod_mem_finset_product, finprod_mem_finset_product', finprod_mem_finset_productβ, finprod_mem_iUnion, finprod_mem_image, finprod_mem_image', finprod_mem_induction, finprod_mem_insert, finprod_mem_insert', finprod_mem_insert_of_eq_one_if_notMem, finprod_mem_insert_one, finprod_mem_inter_mulSupport, finprod_mem_inter_mulSupport_eq, finprod_mem_inter_mulSupport_eq', finprod_mem_inter_mul_diff, finprod_mem_inter_mul_diff', finprod_mem_inv_distrib, finprod_mem_mulSupport, finprod_mem_mul_diff, finprod_mem_mul_diff', finprod_mem_mul_distrib, finprod_mem_mul_distrib', finprod_mem_of_eqOn_one, finprod_mem_one, finprod_mem_pair, finprod_mem_powerset_diff_elem, finprod_mem_powerset_insert, finprod_mem_range, finprod_mem_range', finprod_mem_sUnion, finprod_mem_singleton, finprod_mem_union, finprod_mem_union', finprod_mem_union'', finprod_mem_union_inter, finprod_mem_union_inter', finprod_mem_univ, finprod_mul_distrib, finprod_nonneg, finprod_of_infinite_mulSupport, finprod_of_isEmpty, finprod_one, finprod_option, finprod_pow, finprod_prod_comm, finprod_prod_filter, finprod_set_coe_eq_finprod_mem, finprod_subtype_eq_finprod_cond, finprod_true, finprod_unique, finsum_add_distrib, finsum_apply, finsum_apply_ne_zero, finsum_comp, finsum_comp_equiv, finsum_cond_eq_left, finsum_cond_eq_right, finsum_cond_eq_sum_of_cond_iff, finsum_cond_ne, finsum_cond_pos, finsum_congr, finsum_congr_Prop, finsum_curry, finsum_curryβ, finsum_def, finsum_def', finsum_dmem, finsum_emb_domain, finsum_emb_domain', finsum_eq_dif, finsum_eq_finset_sum_of_support_subset, finsum_eq_if, finsum_eq_indicator_apply, finsum_eq_of_bijective, finsum_eq_single, finsum_eq_sum, finsum_eq_sum_of_fintype, finsum_eq_sum_of_support_subset, finsum_eq_sum_of_support_subset_of_finite, finsum_eq_sum_of_support_toFinset_subset, finsum_eq_sum_plift_of_support_subset, finsum_eq_sum_plift_of_support_toFinset_subset, finsum_eq_zero_of_forall_eq_zero, finsum_false, finsum_induction, finsum_le_finsum', finsum_mem_add_diff, finsum_mem_add_diff', finsum_mem_add_distrib, finsum_mem_add_distrib', finsum_mem_biUnion, finsum_mem_coe_finset, finsum_mem_comm, finsum_mem_congr, finsum_mem_def, finsum_mem_empty, finsum_mem_eq_finite_toFinset_sum, finsum_mem_eq_of_bijOn, finsum_mem_eq_sum, finsum_mem_eq_sum_filter, finsum_mem_eq_sum_of_inter_support_eq, finsum_mem_eq_sum_of_subset, finsum_mem_eq_toFinset_sum, finsum_mem_eq_zero_of_forall_eq_zero, finsum_mem_eq_zero_of_infinite, finsum_mem_finset_eq_sum, finsum_mem_finset_product, finsum_mem_finset_product', finsum_mem_finset_productβ, finsum_mem_iUnion, finsum_mem_image, finsum_mem_image', finsum_mem_induction, finsum_mem_insert, finsum_mem_insert', finsum_mem_insert_of_eq_zero_if_notMem, finsum_mem_insert_zero, finsum_mem_inter_add_diff, finsum_mem_inter_add_diff', finsum_mem_inter_support, finsum_mem_inter_support_eq, finsum_mem_inter_support_eq', finsum_mem_mul, finsum_mem_mul', finsum_mem_neg_distrib, finsum_mem_of_eqOn_zero, finsum_mem_pair, finsum_mem_powerset_diff_elem, finsum_mem_powerset_insert, finsum_mem_range, finsum_mem_range', finsum_mem_sUnion, finsum_mem_singleton, finsum_mem_sub_distrib, finsum_mem_support, finsum_mem_union, finsum_mem_union', finsum_mem_union'', finsum_mem_union_inter, finsum_mem_union_inter', finsum_mem_univ, finsum_mem_zero, finsum_mul, finsum_mul', finsum_neg_distrib, finsum_nonneg, finsum_nsmul, finsum_of_infinite_support, finsum_of_isEmpty, finsum_option, finsum_pos, finsum_pos', finsum_set_coe_eq_finsum_mem, finsum_smul, finsum_smul', finsum_sub_distrib, finsum_subtype_eq_finsum_cond, finsum_sum_comm, finsum_sum_filter, finsum_true, finsum_unique, finsum_zero, map_finprod, map_finset_prod, map_finset_sum, map_finsum, mul_finprod_cond_ne, mul_finsum, mul_finsum', mul_finsum_mem, mul_finsum_mem', nonempty_of_finprod_mem_ne_one, nonempty_of_finsum_mem_ne_zero, one_le_finprod, one_le_finprod', one_lt_finprod, one_lt_finprod', one_lt_finprod_cond, prod_finprod_comm, single_le_finprod, single_le_finsum, smul_finsum, smul_finsum', sum_finsum_comm | 274 |
| Total | 278 |
| Name | Category | Theorems |
|---|
finprod π | CompOp | 180 mathmath: FractionalIdeal.finprod_heightOneSpectrum_factorization_principal, MonoidHom.map_finprod_mem', MulEquivClass.map_finprod, Function.FactorizedRational.divisor, NumberField.prod_nonarchAbsVal_eq, contMDiff_finprod, finprod_mem_union', Height.mulHeightβ_eq, finprod_mem_sUnion, BumpCovering.toPartitionOfUnity_apply, finprod_eq_if, finprod_mem_comm, finprod_mem_insert, finprod_nonneg, NumberField.FinitePlace.prod_eq_inv_abs_norm, finprod_prod_filter, finprod_mem_union, contMDiff_finprod_cond, finprod_mem_finset_product, NumberField.prod_abs_eq_one, finprod_mem_powerset_diff_elem, finprod_mem_dvd, one_le_finprod, finprod_mem_one, Polynomial.monic_finprod_X_sub_C, finprod_mem_range, NumberField.FinitePlace.prod_eq_inv_abs_norm_int, MulEquiv.map_finprod, finprod_emb_domain, finprod_option, prod_finprod_comm, finprod_eq_prod_of_mulSupport_toFinset_subset, finprod_set_coe_eq_finprod_mem, finprod_le_finprod', finprod_mem_mul_diff', finprod_apply_ne_one, finprod_mem_inter_mul_diff, FractionalIdeal.count_finprod_coprime, NumberField.mulHeight_eq, SmoothBumpCovering.toSmoothPartitionOfUnity_apply, FractionalIdeal.finprod_heightOneSpectrum_factorization, MonoidHom.map_finprod_of_preimage_one, finprod_mem_inter_mul_diff', Function.FactorizedRational.meromorphicOrderAt_eq, finprod_mem_of_eqOn_one, finprod_eq_finset_prod_of_mulSupport_subset, FractionalIdeal.count_finprod, finprod_mem_inter_mulSupport_eq', Function.FactorizedRational.finprod_eq_fun, finprod_mul_distrib, map_finprod, finprod_cond_nonneg, finprod_mem_insert_one, MonoidHom.map_finprod_mem, contMDiffAt_finprod, finprod_mem_range', SmoothBumpCovering.sum_toSmoothPartitionOfUnity_eq, finprod_mem_empty, finprod_false, finprod_mem_def, Nat.cast_finprod, finprod_eventually_eq_prod, finprod_mem_mul_distrib', finprod_induction, finprod_mem_eq_prod, finprod_mem_powerset_insert, contMDiffWithinAt_finprod, finprod_curryβ, Function.FactorizedRational.meromorphicNFOn_univ, finprod_def', finprod_cond_eq_right, finprod_prod_comm, finprod_eq_prod_of_fintype, finprod_mem_mulSupport, finprod_mem_union_inter', Function.FactorizedRational.analyticAt, finprod_curry, Height.mulHeight_eq, finprod_mem_insert', finprod_le_finprod, finprod_mem_union'', finprod_subtype_eq_finprod_cond, finprod_true, finprod_cond_ne, finprod_mem_finset_product', finprod_mem_coe_finset, one_lt_finprod', finprod_eq_prod_of_mulSupport_subset_of_finite, finprod_mem_inter_mulSupport_eq, finprod_mem_eq_prod_filter, smul_finprod', finprod_eq_of_bijective, finprod_mem_eq_prod_of_inter_mulSupport_eq, continuous_finprod_cond, finprod_eq_zero, Function.FactorizedRational.meromorphicTrailingCoeffAt_factorizedRational, finprod_pow, finprod_of_infinite_mulSupport, finprod_of_isEmpty, finprod_mem_congr, Function.FactorizedRational.log_norm_meromorphicTrailingCoeffAt, finprod_cond_eq_left, contMDiffOn_finprod, finprod_eq_single, finprod_eq_prod_plift_of_mulSupport_subset, finprod_mem_eq_one_of_infinite, finprod_unique, BumpCovering.sum_toPartitionOfUnity_eq, finprod_congr_Prop, finprod_eq_one_of_forall_eq_one, finprod_mem_eq_prod_of_subset, MeromorphicOn.extract_zeros_poles, finprod_comp_equiv, finprod_mem_union_inter, MonoidHom.map_finprod_Prop, finprod_mem_mul_distrib, finprod_mem_div_distrib, Ideal.finprod_count, finprod_mem_singleton, Function.FactorizedRational.extractFactor, finprod_eq_mulIndicator_apply, finprod_mem_eq_finite_toFinset_prod, tprod_eq_finprod, finprod_mem_iUnion, finprod_apply, analyticAt_finprod, finprod_cond_eq_prod_of_cond_iff, tprod_def, finprod_comp, MonoidHom.map_finprod, Ideal.finprod_heightOneSpectrum_factorization_coe, one_lt_finprod, finprod_mem_biUnion, one_lt_finprod_cond, Nat.cast_finprod_mem, finprod_def, MonoidHom.map_finprod_of_injective, finprod_congr, finprod_mem_image, finprod_eq_prod_plift_of_mulSupport_toFinset_subset, finprod_mem_eq_of_bijOn, finprod_mem_finset_productβ, finprod_mem_image', finprod_mem_finset_eq_prod, NumberField.mulHeightβ_eq, smul_finprod_perm, MonoidHom.map_finprod_plift, Height.AdmissibleAbsValues.product_formula, finprod_mem_inter_mulSupport, tprod_bot, finprod_one, finprod_mem_insert_of_eq_one_if_notMem, FractionalIdeal.finprod_heightOneSpectrum_factorization_principal_fraction, mul_finprod_cond_ne, finprod_eq_dif, Ideal.finprod_not_dvd, finprod_mem_eq_one_of_forall_eq_one, finprod_emb_domain', Function.FactorizedRational.meromorphicTrailingCoeffAt_factorizedRational_off_support, finprod_mem_induction, finprod_mem_pair, finprod_eq_prod_of_mulSupport_subset, BumpCovering.sum_toPOUFun_eq, finprod_div_distrib, finprod_mem_univ, finprod_inv_distrib, Ideal.finprod_heightOneSpectrum_factorization, finprod_dmem, finprod_mem_eq_toFinset_prod, MulEquiv.map_finprod_mem, finprod_mem_mul_diff, FractionalIdeal.finprod_heightOneSpectrum_factorization', Function.FactorizedRational.meromorphicNFOn, one_le_finprod', single_le_finprod, continuous_finprod, finprod_mem_inv_distrib, FractionalIdeal.coeIdeal_finprod, Polynomial.monic_finprod_of_monic, finprod_eq_prod
|
finsum π | CompOp | 216 mathmath: AddMonoidHom.map_finsum_of_injective, finsum_mem_union, MDifferentiableOn.finsum_section_of_locallyFinite, smul_finsum_mem, finsum_mem_insert_zero, PowerSeries.constantCoeff_subst, continuous_finsum, contMDiffOn_finsum, finsum_cond_eq_sum_of_cond_iff, countingFunction_finsum_eq_finsum_add, finsum_eq_sum_plift_of_support_subset, finsum_zero, finsum_one, single_le_finsum, finsum_mem_sub_distrib, SmoothPartitionOfUnity.contMDiffAt_finsum, MvPowerSeries.constantCoeff_subst, finsum_mem_add_diff, ContMDiffAt.finsum_section_of_locallyFinite, finsum_mem_inter_support_eq, finsum_comp_equiv, MDifferentiableWithinAt.finsum_section_of_locallyFinite, AddMonoidHom.map_finsum, finsum_mem_union_inter', finsum_pos, finsum_def', finsum_mem_univ, PowerSeries.coeff_heval, MeromorphicOn.extract_zeros_poles_log, finsum_eq_sum_of_support_subset_of_finite, PowerSeries.coeff_subst, finsum_mem_eq_sum_filter, finsum_mem_inter_add_diff', finsum_mem_support, finsum_mem_mul', finsum_mem_coe_finset, mul_finsum_mem', PartitionOfUnity.sum_eq_one', finsum_sum_filter, finsum_eq_sum, finsum_mem_sUnion, AddMonoidHom.map_finsum_plift, PartitionOfUnity.IsSubordinate.continuous_finsum_smul, tsum_eq_finsum, SmoothPartitionOfUnity.contDiffAt_finsum, Module.rankAtStalk_pi, AddMonoidHom.map_finsum_mem', finsum_sum_comm, Set.encard_iUnion_of_finite, finsum_apply, ContMDiffOn.finsum_section_of_locallyFinite, finsum_mem_eq_sum, sum_finsum_comm, finsum_emb_domain, PartitionOfUnity.sum_le_one', Setoid.IsPartition.ncard_eq_finsum, finsum_eq_of_bijective, finsum_mem_eq_finite_toFinset_sum, finsum_eq_indicator_apply, finsum_nsmul, finsum_sub_distrib, PartitionOfUnity.sum_eq_one, finsum_mem_eq_sum_of_subset, MDifferentiableAt.finsum_section_of_locallyFinite, MvPowerSeries.coeff_subst, SmoothBumpCovering.sum_toSmoothPartitionOfUnity_eq, finsum_option, finsum_eq_if, circleIntegrable_log_norm_factorizedRational, add_finsum_cond_ne, finsum_mem_finset_eq_sum, MvPolynomial.sum_weightedHomogeneousComponent, AddEquiv.map_finsum_mem, Module.Basis.coe_sumCoords_eq_finsum, SmoothPartitionOfUnity.sum_eq_one', finsum_cond_ne, finsum_unique, Nat.cast_finsum, contMDiff_finsum_cond, finsum_mem_eq_zero_of_infinite, PartitionOfUnity.finsum_smul_mem_convex, finsum_of_isEmpty, finsum_dmem, finsum_mem_singleton, ContMDiffWithinAt.finsum_section_of_locallyFinite, finsum_false, mul_finsum', finsum_mem_finset_product', finsum_mem_pair, finsum_congr_Prop, Nat.cast_finsum_mem, finsum_eventually_eq_sum, PartitionOfUnity.sum_finsupport_smul_eq_finsum, Set.encard_iUnion_le_of_finite, SmoothPartitionOfUnity.finsum_smul_mem_convex, finsum_mem_mul, SmoothPartitionOfUnity.sum_le_one', finsum_def, mul_finsum_mem, finsum_mem_congr, ContMDiff.finsum_section_of_locallyFinite, SmoothPartitionOfUnity.sum_nonneg, SkewMonoidAlgebra.coeff_mul_antidiagonal_finsum, PartitionOfUnity.continuous_finsum_smul, finsum_curry, finsum_mem_eq_of_bijOn, map_finsum, finsum_mem_insert, finsum_set_coe_eq_finsum_mem, finsum_mem_zero, finsum_mem_inter_support_eq', finprod_cond_pos, finsum_mem_powerset_insert, SmoothPartitionOfUnity.sum_eq_one, Set.Finite.ncard_biUnion, finsum_apply_ne_zero, MeromorphicOn.circleAverage_log_norm, finsum_mem_insert', finsum_mem_finset_product, MvPolynomial.DirectSum.coeLinearMap_eq_finsum, finsum_mem_range, finsum_true, Function.FactorizedRational.log_norm_meromorphicTrailingCoeffAt, finsum_mem_image', finsum_eq_sum_of_fintype, Set.Finite.ncard_biUnion_le, finsum_mul, contMDiff_finsum, smul_finsum', MeromorphicOn.log_norm_meromorphicTrailingCoeffAt_extract_zeros_poles, finsum_mem_insert_of_eq_zero_if_notMem, finsum_eq_sum_of_support_subset, IntervalIntegrable.finsum, finsum_curryβ, AddMonoidHom.map_finsum_Prop, finsum_mem_powerset_diff_elem, finsum_mem_range', BumpCovering.sum_toPartitionOfUnity_eq, PartitionOfUnity.sum_le_one, finsum_mem_inter_add_diff, finsum_mem_union'', finsum_eq_sum_plift_of_support_toFinset_subset, finsum_of_infinite_support, HahnSeries.SummableFamily.coeff_hsum, finsum_mem_add_distrib, finsum_mem_union_inter, circleAverage_log_norm_factorizedRational, SmoothPartitionOfUnity.sum_finsupport_smul_eq_finsum, SmoothPartitionOfUnity.contMDiff_finsum_smul, Set.ncard_iUnion_of_finite, finsum_pos', finsum_eq_dif, mul_finsum, Commute.isNilpotent_finsum, finsum_mem_add_diff', MDifferentiable.finsum_section_of_locallyFinite, finsum_eq_finset_sum_of_support_subset, PartitionOfUnity.sum_nonneg, PowerSeries.coeff_subst', Set.Finite.encard_biUnion, HahnSeries.SummableFamily.hsum_smulFamily, finsum_cond_eq_right, finsum_mem_add_distrib', finsum_mem_induction, AddEquiv.map_finsum, contMDiffWithinAt_finsum, finsum_mem_neg_distrib, finsum_congr, isNilpotent_finsum, AddEquivClass.map_finsum, finsum_mem_empty, finsum_smul', finsum_mem_biUnion, finsum_induction, finsum_smul, contMDiffAt_finsum, finsum_mem_comm, finsum_le_finsum', finsum_mem_finset_productβ, finsum_eq_zero_of_forall_eq_zero, Group.nat_card_center_add_sum_card_noncenter_eq_card, finsum_add_distrib, finsum_neg_distrib, finsum_mem_of_eqOn_zero, finsum_mul', Set.Finite.encard_biUnion_le, finsum_nonneg, finsum_eq_single, SmoothPartitionOfUnity.IsSubordinate.contMDiff_finsum_smul, finsum_emb_domain', finsum_mem_image, tsum_def, MvPolynomial.finsum_weightedHomogeneousComponent, SmoothPartitionOfUnity.sum_le_one, CircleIntegrable.finsum, AddMonoidHom.map_finsum_mem, finsum_mem_eq_toFinset_sum, tsum_bot, smul_finsum, BumpCovering.sum_toPOUFun_eq, finsum_comp, finsum_mem_eq_sum_of_inter_support_eq, finsum_mem_inter_support, Group.sum_card_conj_classes_eq_card, finsum_cond_eq_left, finsum_mem_eq_zero_of_forall_eq_zero, AddMonoidHom.map_finsum_of_preimage_zero, finsum_mem_iUnion, finsum_mem_def, finsum_cond_pos, SmoothPartitionOfUnity.contMDiff_sum, finsum_eq_sum_of_support_toFinset_subset, continuous_finsum_cond, Set.ncard_iUnion_le_of_finite, finsum_subtype_eq_finsum_cond, finsum_mem_union'
|
Β«termβαΆ _,_Β» π | CompOp | β |
Β«termβαΆ _,_Β» π | CompOp | β |