| Name | Category | Theorems |
|---|
liftAddHom π | CompOp | 7 mathmath: liftAddHom_comp_single, comp_liftAddHom, liftAddHom_apply, liftAddHom_singleAddHom, liftAddHom_apply_single, liftAddHom_symm_apply_apply, liftAddHom_symm_apply
|
prod π | CompOp | 105 mathmath: prod_eq_single, prod_congr, Submonoid.exists_finsupp_of_mem_closure_range, Nat.multiplicative_factorization', Nat.factorization_prod_pow_eq_self, MvPowerSeries.constantCoeff_subst, MvPolynomial.evalβHom_monomial, prod_add_index_of_disjoint, MvPolynomial.monomial_finsupp_sum_index, prod_toMultiset, Nat.prod_pow_pos_of_zero_notMem_support, FractionalIdeal.count_finsuppProd, prod_add_index, MvPolynomial.evalβ_mul_monomial, logb_prod, MvPowerSeries.hasSum_aeval, MvPowerSeries.subst_monomial, onFinset_prod, map_finsuppProd, ArithmeticFunction.IsMultiplicative.multiplicative_factorization, prod_finsetProd_comm, prod_zpow, prod_add_index', Algebra.Generators.H1Cotangent.Ξ΄Aux_monomial, prod_unique, star_finsuppProd, MvPowerSeries.coeff_subst, Nat.eq_factorization_iff, prod_of_support_subset, prod_equivMapDomain, prod_embDomain, Nat.ceilRoot_def, prod_mul, Subgroup.mem_closure_range_iff, prod_indicator_index_eq_prod_attach, RCLike.ofReal_finsuppProd, prod_eq_zero_iff, Rat.cast_finsuppProd, MonoidHom.coe_finsuppProd, MvPowerSeries.evalβ_eq_tsum, prod_inv, prod_mapDomain_index_inj, prod_sumElim, prod_hom_add_index, prod_filter_mul_prod_filter_not, prod_filter_index, MvPolynomial.eval_monomial, prod_indicator_index, Prime.dvd_finsuppProd_iff, MonoidHom.finsuppProd_apply, prod_pow, card_pi, prod_dvd_prod_of_subset_of_dvd, AddOpposite.unop_finsuppProd, Prime.not_dvd_finsuppProd, prod_neg_index, MvPolynomial.monic_monomial_eq, Nat.cast_finsuppProd, AddOpposite.op_finsuppProd, MvPowerSeries.coeff_rescale, Nat.prod_factorization_eq_prod_primeFactors, Nat.prod_pow_factorization_eq_self, prod_option_index, SubmonoidClass.finsuppProd_mem, prod_mapDomain_index, Nat.floorRoot_def, prod_mul_eq_prod_mul_of_exists, prod_div_prod_filter, MvPolynomial.monomial_eq, Nat.totient_eq_prod_factorization, prod_ite_eq, Nat.prod_primeFactors_prod_factorization, prod_mapRange_index, Submonoid.mem_closure_range_iff, prod_fintype, Nat.multiplicative_factorization, log_prod, MvPowerSeries.substAlgHom_monomial, mul_prod_erase, Nat.factorizationEquiv_inv_apply, prod_subtypeDomain_index, prod_sum_index, prod_comm, MvPowerSeries.aeval_eq_sum, MvPowerSeries.monomial_one_eq, MvPolynomial.evalβ_monomial, MvPowerSeries.monomial_eq, Algebra.Generators.Hom.toAlgHom_monomial, MvPowerSeries.coeff_subst_finite, MvPolynomial.aeval_monomial, mul_prod_erase', MvPowerSeries.monomial_smul_const, MvPowerSeries.hasSum_evalβ, Nat.Partition.coeff_genFun, prod_finset_sum_index, prod_single_index, prod_fun_one, MvPowerSeries.monomial_smul_eq, prod_ite_eq', MvPowerSeries.monomial_eq', Int.cast_finsuppProd, Subgroup.exists_finsupp_of_mem_closure_range, prod_zero_index, MvPowerSeries.prod_smul_X_eq_smul_monomial_one, image_pow_eq_finsuppProd_image
|
sum π | CompOp | 216 mathmath: sum_toMultiset, LaurentPolynomial.smeval_eq_sum, AddMonoidAlgebra.lift_apply', MonoidAlgebra.liftMagma_apply_apply, sum_indicator_index, MvPolynomial.totalDegree_monomial, Module.Basis.mem_submodule_iff, sum_indicator_index_eq_sum_attach, AddMonoidAlgebra.mul_apply, Submodule.mem_ideal_smul_span_iff_exists_sum, MvPolynomial.sum_def, MulOpposite.op_finsuppSum, TensorProduct.equivFinsuppOfBasisLeft_symm_apply, sum_apply', multiset_sum_sum_index, sum_zsmul, sum_finsetSum_comm, AddSubgroup.exists_finsupp_of_mem_closure_range, MvPolynomial.monomial_finsupp_sum_index, sum_mapDomain_index_inj, sum_smul_index', MvPolynomial.mul_def, Rat.cast_finsupp_sum, Submodule.mem_iSup_iff_exists_finsupp, groupHomology.mem_cyclesβ_iff, MonoidAlgebra.mul_def, sum_smul_index_linearMap', sum_single_add_single, Algebra.FormallyUnramified.finite_of_free_aux, Sym.coe_equivNatSum_apply_apply, LinearMap.sum_repr_mul_repr_mulββ, AddSubmonoid.mem_closure_range_iff, AddSubmonoid.exists_finsupp_of_mem_closure_range, Submodule.mem_ideal_smul_span_iff_exists_sum', SkewMonoidAlgebra.ofFinsupp_sum, Multiset.toFinsupp_sum_eq, Ideal.finsuppTotal_apply, sum_comm, sum_single_index, Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, sum_zero, sum_equivMapDomain, sum_sub_sum_filter, sum_sub, card_toMultiset, logb_prod, sum_sub_index, Sym.coe_equivNatSum_symm_apply, sum_inner, sum_smul_index, AddSubmonoidClass.finsuppSum_mem, sum_ite_eq, sum_fintype, Submodule.mulLeftMap_apply, toMultiset_apply, TensorProduct.finsuppScalarRight_apply_tmul, QuadraticMap.map_finsuppSum, sum_nonneg, sum_ite_eq', SkewMonoidAlgebra.sum_def, MvPolynomial.scalarRTensor_apply_tmul, sum_congr, Real.log_nat_eq_sum_factorization, sum_mapDomain_index, Int.cast_finsupp_sum, sigma_sum, AddMonoidAlgebra.lift_apply, inner_sum, Real.logb_nat_eq_sum_factorization, sum_filter_add_sum_filter_not, lift_apply, AddMonoidAlgebra.mul_def, subtypeDomain_finsupp_sum, sum_add_index', onFinset_sum, MvPolynomial.rTensor_apply_tmul, AddMonoidHom.finsuppSum_apply, sum_apply'', sum_sum_index', sum_unique, LinearMap.BilinForm.sum_repr_mul_repr_mul, MonoidAlgebra.lift_unique, MvPolynomial.mkDerivationβ_monomial, ArithmeticFunction.cardFactors_eq_sum_factorization, sum_cons, MonoidAlgebra.lift_apply', support_sum, sum_nonneg', sum_filter_index, sum_neg_index, sum_embDomain, Submodule.mem_span_set, RCLike.ofReal_finsupp_sum, TensorProduct.exists_finsupp_left, Orthonormal.inner_finsupp_eq_sum_right, sum_cons', multinomial_update, AddSubgroup.mem_closure_range_iff, sum_add_index_of_disjoint, sum_neg, linearCombination_apply, liftAddHom_apply, HahnSeries.SummableFamily.hsum_ofFinsupp, QuadraticMap.map_finsuppSum', sum_id_lt_of_lt, MvPolynomial.mkDerivation_monomial, AddMonoidAlgebra.mul_apply_left, groupHomology.isBoundaryβ_iff, sum_add, sum_nsmul, lsum_apply, coe_lsum, sum_uncurry_index', MonoidAlgebra.sum_single, sum_curry_index, Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval, AddMonoidAlgebra.liftMagma_apply_apply, LinearMap.finsupp_sum_apply, Submodule.mulRightMap_apply, Orthonormal.inner_finsupp_eq_sum_left, sum_update_add, PointedCone.mem_span_set, TensorProduct.eq_repr_basis_left, sum_uncurry_index, sum_le_sum_index, sum_comapDomain, sum_fun_zero, sum_sumElim, Nat.cast_finsupp_sum, sum_eq_single, LieAlgebra.LoopAlgebra.residuePairing_apply_apply, MonoidAlgebra.lift_apply, sum_hom_add_index, TensorProduct.exists_finsupp_right, add_sum_erase', sum_option_index_smul, TensorProduct.finsuppScalarLeft_apply_tmul, sum_add_eq_sum_add_of_exists, map_finsuppSum, MonoidAlgebra.mul_apply, PolynomialModule.eval_apply, Basis.mem_ideal_iff, mem_span_range_iff_exists_finsupp, MvPolynomial.sum_C, sum_smul_index_semilinearMap', multiset_sum_sum, MvPolynomial.totalDegree_monomial_le, StdSimplex.total, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, sum_subtypeDomain_index, sum_le_sum, multiset_map_sum, log_prod, mul_sum, prod_sum_index, mapDomain_sum, TensorProduct.finsuppLeft_apply_tmul, CategoryTheory.Free.lift_map, MvPolynomial.sum_monomial_eq, MvPolynomial.le_totalDegree, groupHomology.isBoundaryβ_iff, smul_sum, mem_ideal_span_range_iff_exists_finsupp, star_finsuppSum, finTwoArrowEquiv'_sum_eq, MonoidAlgebra.mul_apply_right, sum_mapRange_index, sum_mul, sum_add_index, sum_nonpos, equivFunOnFinite_symm_sum, Submodule.finsuppSum_mem, add_sum_erase, sum_smul_index_addMonoidHom, single_sum, sum_apply, Submodule.mem_span_set_iff_exists_finsupp_le_finrank, coe_sum, AddMonoidAlgebra.lift_unique, Multiset.card_finsuppSum, sum_ite_self_eq', sum_zero_index, Submodule.mem_set_smul, Finset.mem_finsuppAntidiag', MonoidAlgebra.mapDomain_sum, sum_pos', Module.Basis.constr_apply, AddMonoidAlgebra.sum_single, MvPowerSeries.monomial_smul_const, sum_single, sum_finset_sum_index, AddMonoidAlgebra.sum_single_index, Algebra.Generators.comp_Ο, sum_eq_one_iff, TensorProduct.equivFinsuppOfBasisRight_symm_apply, sum_pos, AddMonoidAlgebra.mul_apply_right, MulOpposite.unop_finsuppSum, sum_ite_self_eq, TensorProduct.finsuppRight_apply_tmul, groupHomology.isBoundaryβ_iff, weight_apply, LinearMap.coe_finsupp_sum, sum_mapDomain_index_addMonoidHom, AddMonoidAlgebra.mapDomain_sum, SkewMonoidAlgebra.toFinsupp_sum', groupHomology.mem_cyclesβ_iff, sum_sum_index, MonoidAlgebra.sum_single_index, AddMonoidHom.coe_finsuppSum, sum_of_support_subset, Module.Basis.coe_sumCoords, LinearMap.sum_repr_mul_repr_mul, sum_option_index, TensorProduct.eq_repr_basis_right, MonoidAlgebra.mul_apply_left
|