| Name | Category | Theorems |
|---|
embDomain 📖 | CompOp | 31 mathmath: embDomain_apply, embDomain_some_some, List.toFinsupp_cons_eq_single_add_embDomain, embDomain_mapRange, some_embDomain_some, eq_option_embedding_update_none_iff, embDomain_single, Module.Presentation.directSum_relation, embDomain_injective, MvPolynomial.coeff_rename_embDomain, embDomain_eq_zero, embDomain_comapDomain, prod_embDomain, embDomain_inj, sum_embDomain, linearCombination_embDomain, embDomain_apply_self, Module.Presentation.finsupp_relation, extendDomain_eq_embDomain_subtype, embDomain_add, embDomain_zero, Module.Relations.directSum_relation, Module.Presentation.tensor_relation, embDomain_eq_mapDomain, embDomain_notin_range, embDomain.addMonoidHom_apply, optionEquiv_symm_apply, support_embDomain, List.toFinsupp_append, embDomain_some_none, Module.Relations.tensor_relation
|
equivFunOnFinite 📖 | CompOp | 14 mathmath: equivFunOnFinite_apply, LinearMap.polyCharpolyAux_map_eval, equivFunOnFinite_symm_apply_support, equivFunOnFinite_symm_coe, LinearMap.polyCharpolyAux_map_aeval, finTwoArrowEquiv'_symm_apply, MonoidAlgebra.uniqueRingEquiv_symm_apply, coe_equivFunOnFinite_symm, AddMonoidAlgebra.uniqueRingEquiv_symm_apply, equivFunOnFinite_symm_single, equivFunOnFinite_symm_sum, equivFunOnFinite_single, equivFunOnFinite_symm_eq_sum, equivFunOnFinite_symm_apply_apply
|
instDecidableEq 📖 | CompOp | 36 mathmath: MvPolynomial.support_sum, MvPolynomial.support_mul, MvPolynomial.scalarRTensor_apply_monomial_tmul, MvPowerSeries.coeff_pow, MvPowerSeries.coeff_X_pow, MvPolynomial.scalarRTensor_apply_X_tmul_apply, MvPolynomial.support_sdiff_support_subset_support_add, MvPowerSeries.coeff_X, MvPolynomial.support_add, MvPolynomial.coeff_C, MvPolynomial.support_rename_of_injective, MvPowerSeries.monomial_def, MvPolynomial.support_expand_subset, MvPowerSeries.coeff_inv, MvPolynomial.coeff_X_pow, MvPolynomial.rTensor_apply_X_tmul, MvPowerSeries.coeff_one, MvPowerSeries.coeff_inv_aux, MvPolynomial.support_esymm', MvPolynomial.coeff_one, MvPowerSeries.coeff_prod, MvPolynomial.constantCoeff_monomial, MvPolynomial.image_support_finSuccEquiv, MvPolynomial.support_expand, MvPolynomial.rTensor_apply_monomial_tmul, MvPolynomial.coeff_X', MvPowerSeries.coeff_monomial, MvPowerSeries.coeff_C, MvPolynomial.coeff_rTensorAlgHom_monomial_tmul, MvPowerSeries.coeff_invOfUnit, MvPolynomial.support_sub, MvPolynomial.support_esymm'', MvPolynomial.coeff_monomial, Finset.finsuppAntidiag_insert, MvPolynomial.support_symmDiff_support_subset_support_add, MvPolynomial.support_esymm
|
instFunLike 📖 | CompOp | 733 mathmath: coe_neg, MvPolynomial.pUnitAlgEquiv_symm_monomial, TensorProduct.finsuppRight_apply, AddMonoidAlgebra.modOf_apply_add_self, snd_sumFinsuppLEquivProdFinsupp, range_subset_insert_frange, fst_sumFinsuppLEquivProdFinsupp, linearCombination_apply_of_mem_supported, AddMonoidAlgebra.mul_single_apply, mapRange_apply, coe_sumElim, AddMonoidAlgebra.mapDomainRingEquiv_apply, Orthonormal.inner_left_finsupp, degree_eq_sum, AddMonoidAlgebra.mul_apply, embDomain_apply, Nat.Prime.exists_orderOf_eq_pow_factorization_exponent, embDomain_some_some, Nat.Primes.prodNatEquiv_symm_apply, Nat.multiplicity_eq_factorization, Nat.factorization_eq_zero_of_not_dvd, IsPrimePow.exists_ordCompl_eq_one, MvPolynomial.support_finSuccEquiv, MvPolynomial.rTensor_apply_tmul_apply, Nat.Prime.factorization_pos_of_dvd, sumElim_inr, SkewMonoidAlgebra.toFinsupp_apply, sub_apply, card_Ioc, MvPolynomial.mem_image_support_coeff_finSuccEquiv, MvPolynomial.scalarRTensor_apply_monomial_tmul, Module.basisUnique_repr_eq_zero_iff, Nat.ordCompl_le, MvPolynomial.weightedDegree_eq_zero_iff, finsuppTensorFinsupp_apply, onFinset_apply, IsPrimePow.minFac_pow_factorization_eq, coe_le_coe, NumberField.Units.fun_eq_repr, IsBaseChange.basis_repr_comp_apply, Module.Basis.toDual_linearCombination_left, IsAdjoinRootMonic.coeff_apply, LinearMap.toMatrix_apply', card_Ico, filter_apply_neg, Matrix.repr_toLin, MvPowerSeries.coeff_pow, PolynomialModule.add_apply, mem_frange_of_mem, sumElim_apply, sum_zsmul, sumFinsuppAddEquivProdFinsupp_symm_inl, AddMonoidAlgebra.mapRangeAddEquiv_apply, erase_same, AList.lookupFinsupp_eq_zero_iff, exteriorPower.basis_repr_ne, if_mem_support, filter_apply_pos, weight_single_one_apply, linearEquivFunOnFinite_symm_coe, Module.Basis.repr_isUnitSMul, Submodule.mem_iSup_iff_exists_finsupp, single_eq_same, coe_ceilDiv_def, filter_eq_indicator, equivFunOnFinite_apply, AddMonoidAlgebra.mapDomainAddEquiv_apply, MvPolynomial.scalarRTensor_apply_X_tmul_apply, Nat.factorization_eq_of_coprime_right, Nat.factorization_mul_apply_of_coprime, Algebra.FormallyUnramified.finite_of_free_aux, Module.Basis.prod_repr_inl, Nat.ordCompl_dvd_ordCompl_iff_dvd, Sym.coe_equivNatSum_apply_apply, sigmaFinsuppAddEquivPiFinsupp_apply, Nat.ordProj_of_not_prime, Finset.mem_finsuppAntidiag, MonoidAlgebra.single_one_mul_apply, Module.Basis.repr_self_apply, mem_range_mapDomain_iff, FractionalIdeal.count_finsuppProd, Nat.pow_succ_factorization_not_dvd, IsLocalFrameOn.coeff_apply_of_mem, single_smul, Representation.ofMulAction_apply, Ideal.Filtration.mem_submodule, finTwoArrowEquiv'_apply, Ideal.finsuppTotal_apply_eq_of_fintype, erase_ne, IntermediateField.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, MvPolynomial.supDegree_esymmAlgHomMonomial, PowerSeries.coeff_heval, eq_single_iff, coeFnAddHom_apply, curryLinearEquiv_symm_apply_apply, AddMonoidAlgebra.single_apply, Nat.factorization_factorial, erase_apply, ext_iff', TensorProduct.equivFinsuppOfBasisLeft_apply_tmul_apply, notMem_support_iff, AddMonoidAlgebra.uniqueRingEquiv_apply, fun_support_eq, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, univ_sum_single_apply', MonoidAlgebra.uniqueRingEquiv_apply, basis_repr, Matrix.toBilin_apply, IsLocalRing.basisQuotient_repr, List.toFinsupp_apply_fin, Polynomial.coeff_ofFinsupp, update_self, LinearMap.toMatrixAlgEquiv_apply, NumberField.mixedEmbedding.stdBasis_apply_isComplex_snd, Nat.ordCompl_dvd_ordCompl_of_dvd, cons_succ, LinearMap.BilinForm.apply_eq_dotProduct_toMatrix_mulVec, AddMonoidAlgebra.divOf_apply, IsAdjoinRootMonic.basis_repr, finite_support, eq_option_embedding_update_none_iff, MvPolynomial.X_mul_pderiv_monomial, Module.Basis.ofEquivFun_repr_apply, Module.Basis.reindexRange_repr', sum_ite_eq, Ordinal.CNF.coeff_zero_apply, indicator_of_notMem, optionElim_some, sum_fintype, Module.Basis.reindexRange_repr, mem_rangeSingleton_apply_iff, sigmaFinsuppLEquivPiFinsupp_symm_apply, Nat.factorization_eq_card_pow_dvd_of_lt, MonoidAlgebra.single_mul_apply, AddMonoidAlgebra.neg_apply, TensorProduct.finsuppScalarRight_apply, zipWith_apply, BoundedContinuousFunction.mem_charPoly, BoundedContinuousFunction.charAlgHom_apply, coe_pointwise_smul, Ordinal.CNF.coeff_of_not_mem_CNF, Polynomial.derivativeFinsupp_apply_toFun, Nat.ordProj_dvd_ordProj_iff_dvd, single_eq_of_ne, NumberField.canonicalEmbedding.integralBasis_repr_apply, Finset.sum_apply', Nat.exists_factorization_lt_of_lt, QuadraticMap.map_finsuppSum, lcoeFun_apply, Nat.factorization_eq_one_of_squarefree, unique_single, le_def, Nat.factorization_choose_prime_pow_add_factorization, Module.Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul, floorDiv_apply, sum_ite_eq', Nat.factorization_prod_apply, update_apply, prod_zpow, rangeIcc_toFun, ZSpan.repr_ceil_apply, AddMonoidAlgebra.mapRangeRingHom_apply, add_apply, Finset.mem_finsupp_iff, indicator_apply, MvPolynomial.degreeOf_le_iff, Module.Basis.addSubgroupOfClosure_repr_apply, basis_toMatrix_basisFun_mul, Nat.factorization_one_right, finite_range, lex_iff_of_unique, linearEquivFunOnFinite_symm_apply, toDFinsupp_coe, MonomialOrder.lex_lt_iff_of_unique, finsuppTensorFinsupp'_apply_apply, finset_sum_apply, uncurry_apply, Ordinal.CNF.coeff_of_mem_CNF, single_eq_of_ne', PolynomialModule.single_apply, single_apply_left, le_iff, mem_submodule_iff, Module.Basis.sumQuot_repr_inl, sigmaFinsuppEquivPiFinsupp_apply, Nat.ordProj_mul_ordCompl_eq_self, Nat.pairwise_coprime_pow_primeFactors_factorization, LaurentPolynomial.C_apply, coe_neLocus, Algebra.Generators.cotangentSpaceBasis_repr_tmul, MvPolynomial.mem_support_notMem_vars_zero, AddMonoidAlgebra.modOf_apply_of_not_exists_add, sumFinsuppLEquivProdFinsupp_symm_inl, LaurentPolynomial.T_apply, ceilDiv_apply, List.coe_toFinsupp, MvPolynomial.rTensor_apply_X_tmul, MonoidAlgebra.mapRangeAlgHom_apply, MvPolynomial.eval_eq', PiLp.basisFun_repr, degree_apply, linearCombination_single_index, prod_unique, Nat.factorization_choose_le_one, TensorProduct.equivFinsuppOfBasisRight_apply_tmul_apply, Multiset.toFinsupp_apply, MonoidAlgebra.single_mul_apply_aux, Equiv.finsuppUnique_apply, single_eq_update, optionElim_eq_elim', apply_surjective, sigmaFinsuppEquivDFinsupp_symm_apply, Polynomial.derivativeFinsupp_apply_apply, Nat.dvd_ordCompl_of_dvd_not_dvd, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, AddEquiv.finsuppUnique_apply, Nat.Prime.dvd_iff_one_le_factorization, MvPolynomial.eq_modMonomial_single_iff, Module.Basis.linearCombination_dualBasis, prod_of_support_subset, FiniteDimensional.basisSingleton_repr_apply, le_degree, Module.Basis.equivFunL_symm_apply_repr, PowerBasis.repr_gen_pow_isIntegral, card_Icc, sum_unique, Subalgebra.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, Module.Basis.smulTower'_repr_mk, rangeIcc_apply, Matrix.GeneralLinearGroup.toLin'_apply, le_weight, AList.lookupFinsupp_eq_iff_of_ne_zero, Finset.mem_finsupp_iff_of_support_subset, MvPolynomial.exists_degree_lt, card_uIcc, card_Ioo, support_sum, mk_mem_graph_iff, Module.Basis.algebraMapCoeffs_repr_apply_toFun, LinearMap.toMatrix_mulVec_repr, sum_filter_index, AddMonoidAlgebra.apply_add_of_supDegree_le, single_eq_set_indicator, filter_eq_sum, snd_sumFinsuppAddEquivProdFinsupp, Matrix.toLin_apply_eq_zero_iff, erase_eq_sub_single, AddMonoidAlgebra.modOf_apply_of_exists_add, linearDepOn_iff, AddMonoidAlgebra.coe_add, DFinsupp.toFinsupp_coe, Module.Basis.algebraMapCoeffs_repr_apply_apply, Matrix.toLinearMapₛₗ₂_apply, LinearMap.BilinForm.dualBasis_repr_apply, support_subset_singleton, filter_eq_zero_iff, PolynomialModule.zero_apply, Module.Basis.sumQuot_repr_inl_of_mem, Module.End.ringEquivEndFinsupp_apply_apply_apply, Nat.exponent_eq_exponent_mul_factorization_of_prime_pow_eq_base_pow, sumFinsuppEquivProdFinsupp_symm_inr, TensorProduct.finsuppScalarRight_apply_tmul_apply, AddMonoidAlgebra.mul_single_zero_apply, apply_eq_dotProduct_toMatrix₂_mulVec, TensorProduct.finsuppLeft_apply, MvPolynomial.weightedTotalDegree_eq_zero_iff, inf_apply, Module.Basis.restrictScalars_repr_apply, Orthonormal.inner_finsupp_eq_sum_right, Module.Basis.equivFunL_apply, Nat.factorization_centralBinom_eq_zero_of_two_mul_lt, prod_eq_zero_iff, Squarefree.natFactorization_le_one, MvPolynomial.monomial_le_degreeOf, MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination, MonoidAlgebra.mapRangeAddEquiv_apply, MvPolynomial.coeff_sumSMulX, multinomial_eq_of_support_subset, Nat.factorization_choose_of_lt_three_mul, multinomial_update, Module.Basis.singleton_repr, count_toMultiset, MonoidAlgebra.coe_add, MvPolynomial.mem_restrictDegree, LinearMap.polyCharpolyAux_map_eq_charpoly, LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff, MvPolynomial.supDegree_esymm, Nat.factorization_lt, LinearMap.toMatrix_transpose_apply, Pi.basis_repr, cons_tail, MvPolynomial.eval_eq, MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul, Nat.not_dvd_ordCompl, InnerProductSpace.gramSchmidt_triangular, QuadraticAlgebra.basis_repr_apply, Module.Basis.toDual_eq_repr, weight_single_index, Module.Basis.sum_repr_mul_repr, prod_filter_index, NumberField.integralBasis_repr_apply, MvPolynomial.eval₂_eq', fst_sumFinsuppEquivProdFinsupp, smul_apply, ArithmeticFunction.sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul, Colex.le_iff_of_unique, Lex.le_iff_of_unique, coe_update, comapDomain_apply, support_eq_singleton, mul_apply, mapDomain_apply, QuadraticMap.map_finsuppSum', univ_sum_single_apply, PiTensorProduct.ofFinsuppEquiv_apply, equivFunOnFinite_symm_coe, lt_def, Equiv.finsuppUnique_symm_apply_apply, NumberField.mixedEmbedding.stdBasis_apply_isComplex_fst, lex_lt_iff_of_unique, Module.Basis.localizationLocalization_repr_algebraMap, Module.Basis.dualBasis_apply, apply_eq_star_dotProduct_toMatrix₂_mulVec, Complex.coe_basisOneI_repr, embDomain_apply_self, ofSupportFinite_fin_two_eq, MvPolynomial.schwartz_zippel_sup_sum, PolynomialModule.smul_apply, AddMonoidAlgebra.mul_apply_left, orderEmbeddingToFun_apply, Orthonormal.inner_right_finsupp, LinearMap.toMatrix_transpose_apply', piecewise_apply, HahnSeries.coeff_ofFinsupp, coe_onFinset, sum_nsmul, Nat.primeFactorsList_count_eq, LinearMap.toMatrix_smulRight, single_apply_eq_zero, subtypeDomain_apply, Prime.dvd_finsuppProd_iff, Nat.setOf_pow_dvd_eq_Icc_factorization, NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, lex_lt_of_lt, single_swap, AdjoinRoot.powerBasisAux'_repr_symm_apply, MvPowerSeries.coeff_prod, coe_finset_sum, Nat.factorization_choose', AddMonoidAlgebra.coeff_smul, Basis.multilinearMap_apply_apply, Nat.factorization_choose_le_log, Nat.factorization_eq_zero_of_not_prime, Module.Basis.coe_finTwoProd_repr, linearCombination_unique, PolynomialModule.smul_single_apply, MvPolynomial.prod_X_pow_eq_monomial, multinomial_eq, MonoidAlgebra.mapRangeRingEquiv_apply, IsAdjoinRootMonic.coeff_apply_lt, Nat.Icc_factorization_eq_pow_dvd, mem_rangeIcc_apply_iff, Representation.apply_eq_of_leftRegular_eq_of_generator, Nat.ordCompl_pos, DirectSum.IsInternal.collectedBasis_repr_of_mem_ne, Module.Basis.toMatrix_apply, KaehlerDifferential.mvPolynomialBasis_repr_apply, MvPolynomial.optionEquivLeft_coeff_some_coeff_none, sigmaFinsuppLEquivPiFinsupp_apply, Nat.ordCompl_mul, Nat.ordProj_le, Algebra.toMatrix_lmul', AddMonoidAlgebra.single_mul_apply, Nat.factorization_le_factorization_choose_add, Module.DualBases.dual_lc, MvPolynomial.exists_mem_support_not_dvd_of_forall_totalDegree_le, Colex.lt_iff, TensorProduct.finsuppScalarLeft_apply_tmul_apply, AddMonoidAlgebra.modOf_apply_self_add, apply_single', equivMapDomain_symm_apply, MonoidAlgebra.smul_apply, prod_pow, mk_mem_graph, coe_add, nsmul_apply, Nat.card_divisors, ZLattice.exists_forall_abs_repr_le_norm, Nat.Prime.factorization_self, AddMonoidAlgebra.single_mul_apply_of_not_exists_add, card_pi, Matrix.toLin_apply, MvPolynomial.totalDegree_eq_zero_iff, MultilinearMap.freeFinsuppEquiv_apply, AddMonoidAlgebra.apply_eq_zero_of_not_le_supDegree, filter_apply, Nat.ordProj_dvd_ordProj_of_dvd, coe_smul, MvPolynomial.mem_support_finSuccEquiv, comapSMul_apply, Orthonormal.inner_finsupp_eq_sum_left, Sylow.card_eq_multiplicity, subtypeDomain_eq_zero_iff', lapply_apply, fst_sumFinsuppAddEquivProdFinsupp, Nat.factorization_centralBinom_of_two_mul_self_lt_three_mul, zero_apply, MvPolynomial.degreeOf_eq_sup, ofSupportFinite_coe, Module.Basis.sumQuot_repr_inr_of_mem, List.toFinsupp_apply_le, Nat.ordCompl_self_pow_mul, MonoidAlgebra.mul_single_apply_of_not_exists_mul, Pi.counit_coe_finsupp, MvPolynomial.image_support_finSuccEquiv, AddMonoidAlgebra.mul_single_apply_aux, NumberField.inverse_basisMatrix_mulVec_eq_repr, sum_update_add, coe_nsmul, embSigma_apply_of_ne, erase_add_single, MonoidAlgebra.mul_single_one_apply, LaurentPolynomial.ext_iff, PointedCone.mem_span_set, MultilinearMap.freeFinsuppEquiv_single, InnerProductSpace.toMatrix_rankOne, update_eq_sub_add_single, AddMonoidAlgebra.mul_apply_add_eq_mul_of_uniqueAdd, MvPolynomial.pderiv_monomial, coe_sym2Mul, Nat.prod_pow_primeFactors_factorization, equivMapDomain_apply, single_add_erase, LinearMap.polyCharpolyAux_coeff_eval, coe_eq_zero, rangeSingleton_apply, Matrix.toLinAlgEquiv_apply, MonomialOrder.div_set, MvPolynomial.support_optionEquivLeft, TensorProduct.equivFinsuppOfBasisRight_apply, le_iff', Nat.ordProj_self_pow, univ_sum_single, exists_ordCompl_eq_one_iff_isPrimePow, PowerSeries.coeff_prod, Nat.prod_factorization_eq_prod_primeFactors, Nat.factorization_eq_zero_iff_remainder, List.toFinsupp_apply_lt, Matrix.toLinearMap₂_apply, linearEquivFunOnFinite_apply, Nat.Prime.pow_dvd_iff_dvd_ordProj, ZLattice.abs_repr_lt_of_norm_lt, optionElim_apply_some, prod_option_index, LieAlgebra.LoopAlgebra.residuePairing_apply_apply, MvPolynomial.rTensor_apply_monomial_tmul, Algebra.Generators.repr_CotangentSpaceMap, Module.Basis.dualBasis_repr, sumFinsuppLEquivProdFinsupp_symm_inr, Pi.comul_coe_finsupp, NumberField.mixedEmbedding.stdBasis_apply_isReal, coe_rangeIcc, PolynomialModule.lsingle_apply, Module.Basis.linearCombination_coord, sup_apply, coe_floorDiv, cons_zero, Module.Basis.equivFun_apply, add_sum_erase', sum_option_index_smul, coe_equivFunOnFinite_symm, Module.Basis.smulTower'_repr, apply_single, MonoidAlgebra.mul_apply, LinearEquiv.finsuppUnique_apply, applyAddHom_apply, mapDomain_equiv_apply, exteriorPower.basis_repr_apply, Module.Basis.toMatrix_update, range_single_subset, PiLp.basis_toMatrix_basisFun_mul, subtypeDomain_eq_iff_forall, Polynomial.toFinsupp_apply, neg_apply, Module.Basis.baseChange_repr_tmul, SkewMonoidAlgebra.coeff_ofFinsupp, lex_le_iff_of_unique, ZSpan.repr_fract_apply, finsuppLEquivDirectSum_apply, LinearMap.polyCharpoly_map_eq_charpoly, finsuppTensorFinsuppLid_apply_apply, LaurentPolynomial.invert_apply, single_apply_mem, QuaternionAlgebra.coe_basisOneIJK_repr, Nat.factorization_choose_eq_zero_of_lt, centralBinom_factorization_small, Nat.prod_pow_factorization_choose, logHeight_eq_log_mulHeight, uncurry_apply_pair, Nat.factorization_prime_le_iff_dvd, coe_lt_coe, Nat.sum_divisors, prod_ite_eq, AddMonoidAlgebra.mapRangeRingEquiv_apply, extendDomain_toFun, card_Iic, Nat.factorization_pow_self, optionElim_apply_eq_elim, single_le_iff, split_apply, NumberField.mixedEmbedding.latticeBasis_repr_apply, card_Iio, smul_eq, Module.Basis.ext_elem_iff, MonoidAlgebra.mapDomainRingEquiv_apply, Nat.factorization_eq_card_pow_dvd, prod_fintype, finsuppTensorFinsuppRid_apply_apply, Module.Basis.repr_sum_self, linearCombination_option, Algebra.leftMulMatrix_mulVec_repr, factorization_eq_count, Nat.factorization_factorial_mul_succ, Module.Basis.smulTower_repr_mk, Algebra.Generators.cotangentRestrict_mk, Nat.factorization_ordCompl, MvPolynomial.optionEquivLeft_monomial, lex_lt_iff, Polynomial.coeff_homogenize, mul_prod_erase, Derivation.mapCoeffs_apply, tsub_apply, embSigma_apply_self, embDomain_notin_range, AddMonoidAlgebra.ext_iff, single_apply, sumFinsuppEquivProdFinsupp_symm_inl, lex_def, single_add_apply, Module.Basis.SmithNormalForm.repr_comp_embedding_eq_smul, Nat.sub_one_mul_factorization_factorial, Module.Basis.toDual_linearCombination_right, PiTensorProduct.ofFinsuppEquiv'_apply_apply, AddMonoidAlgebra.single_zero_mul_apply, smul_apply_addAction, Nat.ordProj_dvd, LinearMap.toMatrix_toSpanSingleton, MonoidAlgebra.ext_iff, unique_ext_iff, linearDepOn_iffₛ, Icc_eq, addCommute_iff_inter, MvPolynomial.pUnitAlgEquiv_monomial, MvPolynomial.eval₂_eq, Nat.factorization_def, AddMonoidAlgebra.domCongr_apply, OrthonormalBasis.coe_toBasis_repr_apply, Nat.coprime_ordCompl, ZLattice.normBound_spec, QuadraticMap.apply_linearCombination, Nat.Prime.pow_dvd_iff_le_factorization, embSigma_apply, AdjoinRoot.powerBasisAux'_repr_apply_to_fun, IsAdjoinRootMonic.coeff_apply_coe, Module.Basis.traceDual_repr_apply, Nat.factorization_factorial_le_div_pred, AddMonoidAlgebra.single_mul_apply_aux, Module.Basis.ofZLatticeComap_repr_apply, coe_univ_sum_single, Module.End.ringEquivEndFinsupp_apply_apply_support, coe_tsub, PolynomialModule.monomial_smul_apply, LinearMap.toMvPolynomial_eval_eq_apply, Module.Basis.toMatrix_transpose_apply, HahnSeries.SummableFamily.coeff_apply, indicator_of_mem, Nat.dvd_ordProj_of_dvd, sumFinsuppAddEquivProdFinsupp_symm_inr, Nat.ordProj_pos, MonoidAlgebra.mul_apply_right, Nat.ordCompl_eq_self_iff_zero_or_not_dvd, Module.Basis.ofZLatticeBasis_repr_apply, Nat.ordProj_mul, Nat.factorization_eq_zero_of_remainder, mem_graph_iff, tail_apply, LinearMap.toMatrixAlgEquiv_apply', MonomialOrder.div, IntermediateField.LinearDisjoint.basisOfBasisLeft_repr_apply, TensorProduct.equivFinsuppOfBasisLeft_apply, Module.Basis.prod_repr_inr, support_subset_iff, extendDomain_apply, AddEquiv.finsuppUnique_symm_apply_apply, add_sum_erase, Nat.factorization_choose_prime_pow, ArithmeticFunction.carmichael_factorization, sum_apply, BilinForm.apply_eq_dotProduct_toMatrix_mulVec, Nat.factorization_choose, MvPolynomial.IsSymmetric.antitone_supDegree, coe_sum, Module.Basis.toDual_apply_left, optionEquiv_apply, QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar, MvPolynomial.rTensor_apply, card_support_le_one, single_eq_pi_single, MonoidAlgebra.mapDomainAddEquiv_apply, coe_mul, sum_ite_self_eq', Nat.factorization_eq_zero_iff, NumberField.canonicalEmbedding_eq_basisMatrix_mulVec, coe_mk, MonoidAlgebra.mul_single_apply, AList.lookupFinsupp_apply, Module.Basis.reindexFinsetRange_repr, mem_frange, Module.Basis.continuous_coe_repr, sym2Mul_apply_mk, mapDomain_apply', TensorProduct.finsuppScalarLeft_apply, Module.Basis.smulTower_repr, Module.Basis.toDual_apply_right, linearCombination_comapDomain, Module.DualBases.coeffs_apply, Nat.Prime.exists_addOrderOf_eq_pow_padic_val_nat_add_exponent, Nat.factorization_eq_zero_of_non_prime, List.toFinsupp_apply, ZSpan.repr_floor_apply, coe_sub, MonoidAlgebra.single_apply, Module.Basis.tensorProduct_repr_tmul_apply, Nat.prod_pow_factorization_centralBinom, Basis.piTensorProduct_repr_tprod_apply, mul_prod_erase', Module.Basis.repr_smul', Lex.lt_iff, Module.Basis.repr_unitsSMul, PowerSeries.coeff_pow, Nat.ordCompl_dvd, MonoidAlgebra.mul_apply_antidiagonal, ext_iff, Nat.factorization_eq_zero_of_lt, Subalgebra.LinearDisjoint.basisOfBasisLeft_repr_apply, optionElim_apply_none, snd_sumFinsuppEquivProdFinsupp, Module.End.ringEquivEndFinsupp_symm_apply_apply, supportedEquivFinsupp_symm_apply_coe_apply, sumElim_inl, MonoidAlgebra.single_mul_apply_of_not_exists_mul, Module.Basis.norm_repr_le_norm, MvPolynomial.scalarRTensor_apply_tmul_apply, Pi.basisFun_repr, Algebra.leftMulMatrix_eq_repr_mul, apply_eq_of_mem_graph, finsuppProdLEquiv_symm_apply_apply, Module.Basis.sum_repr, HahnSeries.SummableFamily.coeff_def, supportedEquivFinsupp_apply_apply, ZSpan.mem_fundamentalDomain, Module.Basis.toMatrix_mulVec_repr, lex_lt_of_lt_of_preorder, Module.Basis.coord_apply, Module.Basis.mem_span_iff_repr_mem, Module.Basis.SmithNormalForm.repr_eq_zero_of_notMem_range, AddMonoidAlgebra.mul_apply_right, notMem_neLocus, Colex.lt_iff_of_unique, embDomain_some_none, prod_ite_eq', some_apply, LinearMap.toMatrixAlgEquiv_transpose_apply, MonoidAlgebra.domCongr_apply, TensorProduct.finsuppRight_apply_tmul_apply, sum_ite_self_eq, MvPolynomial.degreeOf_monomial_eq, isPrimePow_iff_minFac_pow_factorization_eq, Polynomial.degreeLT.basis_repr, coe_zero, Nat.ordCompl_self_pow, AddMonoidAlgebra.mul_single_apply_of_not_exists_add, Module.Basis.repr_reindex_apply, degree_def, LinearMap.toMatrix_apply, Nat.factorization_zero_right, NumberField.house.basis_repr_norm_le_const_mul_house, MonoidAlgebra.neg_apply, Set.indicator_singleton_eq, Nat.pow_factorization_choose_le, AddMonoidAlgebra.mapRangeAlgHom_apply, Nat.factorization_le_of_le_pow, Lex.lt_iff_of_unique, LinearMap.toMatrixAlgEquiv_transpose_apply', instCanLift, Nat.factorization_eq_of_coprime_left, MvPolynomial.bind₁_monomial, LinearMap.polyCharpoly_coeff_eval, MvPolynomial.degreeOf_lt_iff, HahnSeries.SummableFamily.coe_ofFinsupp, sum_of_support_subset, mem_pi, exteriorPower.basis_repr_self, card_support_eq_one, Pi.lex_eq_finsupp_lex, HahnSeries.coeff_ofFinsuppLinearMap, Module.Basis.sumQuot_repr_inr, AddMonoidAlgebra.mul_apply_antidiagonal, Module.Basis.coord_repr_symm, lcongr_apply_apply, Nat.factorization_le_factorization_of_dvd_right, Nat.ordCompl_of_not_prime, MonomialOrder.lex_le_iff_of_unique, Nat.factorization_factorial_mul, MonoidAlgebra.mul_single_apply_aux, ZLattice.abs_repr_le, DirectSum.IsInternal.collectedBasis_repr_of_mem, equivFunOnFinite_symm_apply_apply, Nat.squarefree_iff_factorization_le_one, mem_supported', MonoidAlgebra.mapRangeRingHom_apply, Module.Basis.ofIsLocalizedModule_repr_apply, AddMonoidAlgebra.apply_supDegree_add_supDegree, single_of_single_apply, LinearMap.fst_prodOfFinsuppNat, TensorProduct.finsuppLeft_apply_tmul_apply, LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly, sym2_support_eq_preimage_support_mul, mapDomain_notin_range, sum_option_index, curry_apply, Nat.factorization_factorial_eq_zero_of_lt, MonoidAlgebra.mul_apply_left
|
instInhabited 📖 | CompOp | 5 mathmath: MvPolynomial.leadingCoeff_esymmAlgHomMonomial, MvPolynomial.leadingCoeff_toLex_C, MvPolynomial.monic_esymm, default_eq_zero, MvPolynomial.leadingCoeff_toLex
|
instZero 📖 | CompOp | 223 mathmath: instSMulPosReflectLE, MvPowerSeries.coeff_zero_eq_constantCoeff_apply, SkewMonoidAlgebra.ofFinsupp_eq_zero, MvPowerSeries.coeff_zero_eq_constantCoeff, IsSMulRegular.finsupp, zero_update, instPosSMulReflectLE, sigmaFinsuppEquivDFinsupp_support, List.toFinsupp_eq_sum_mapIdx_single, SkewMonoidAlgebra.ofFinsupp_zero, MvPolynomial.one_def, SkewMonoidAlgebra.ofFinsupp_smul, curryEquiv_apply, filter_smul, Rep.diagonalSuccIsoFree_inv_hom_single, MonomialOrder.degree_monomial, SkewMonoidAlgebra.toFinsupp_smul, embSigma_zero, sigmaFinsuppAddEquivDFinsupp_apply, sum_smul_index', bot_eq_zero, toMultiset_zero, sum_smul_index_linearMap', smulCommClass, support_zero, comapDomain_smul_of_injective, Rep.finsuppToCoinvariantsTensorFree_single, Rep.coinvariantsTensorFreeLEquiv_symm_apply, curryLinearEquiv_symm_apply_apply, linearCombination_smul, linearIndepOn_iff, some_zero, sigmaFinsuppAddEquivDFinsupp_symm_apply, MvPolynomial.weightedHomogeneousComponent_zero, Algebra.TensorProduct.basis_repr_tmul, sum_smul_index, Rep.diagonalSuccIsoFree_inv_hom_single_single, Representation.leftRegular_norm_eq_zero_iff, TensorProduct.finsuppLeft_smul', Algebra.TensorProduct.basisAux_map_smul, single_eq_zero, MvPolynomial.C_apply, filter_curry, add_eq_zero_iff, sigmaFinsuppEquivDFinsupp_add, MvPolynomial.coeff_C, DFinsupp.toFinsupp_smul, mapRange_smul, MvPolynomial.isUnit_iff_totalDegree_of_isReduced, neLocus_zero_left, Module.Basis.isScalarTower_finsupp, MvPolynomial.isUnit_iff, Rep.coinvariantsTensorFreeLEquiv_apply, uncurry_apply, MvPowerSeries.monomial_zero_eq_C, MvPowerSeries.coeff_inv, MvPolynomial.coeff_zero_C, StdSimplex.nonneg, embSigma_eq_zero, embDomain_eq_zero, sigmaFinsuppEquivDFinsupp_symm_apply, instFaithfulSMulOfNonempty, LinearMap.CompatibleSMul.finsupp_dom, TensorProduct.finsuppScalarRight_smul, MonomialOrder.degree_subsingleton, Nat.factorization_zero, instSMulPosReflectLT, AList.empty_lookupFinsupp, MvPowerSeries.coeff_one, filter_eq_zero_iff, curry_single, Rep.freeLiftLEquiv_apply, coe_curryAddEquiv, factorization_zero, MvPolynomial.totalDegree_eq_zero_iff_eq_C, uncurry_single, instSMulPosMono, mapDomain_zero, Algebra.TensorProduct.basisAux_tmul, MvPowerSeries.monomial_zero_eq_C_apply, MvPolynomial.restrictSupport_zero, sigmaFinsuppEquivDFinsupp_smul, instPosSMulStrictMono, smul_single', split_embSigma_of_ne, MonomialOrder.degree_C, smul_apply, MvPolynomial.coeff_zero_X, MvPowerSeries.coeff_zero_mul_X, MvPowerSeries.coeff_inv_aux, erase_zero, single_nonpos, LinearMap.CompatibleSMul.finsupp_cod, groupHomology.inhomogeneousChains.d_single, equivMapDomain_zero, HahnSeries.coeff_ofFinsupp, MvPolynomial.eq_C_of_isEmpty, MvPolynomial.coeff_one, MvPolynomial.monomial_zero', SkewMonoidAlgebra.toFinsupp_zero, filter_single_of_neg, neLocus_zero_right, isCentralScalar, sum_uncurry_index', List.support_sum_eq, MvPolynomial.constantCoeff_monomial, MvPolynomial.supDegree_toLex_C, MvPowerSeries.coeff_zero_one, sum_curry_index, MonomialOrder.degree_one, MultilinearMap.freeFinsuppEquiv_apply, mapRange_smul', coe_smul, MvPolynomial.restrictSupport_nsmul, some_single_none, subtypeDomain_eq_zero_iff', MvPowerSeries.coeff_zero_X_mul, MvPolynomial.esymmAlgHom_zero, zero_apply, MvPolynomial.homogeneousComponent_zero, MonomialOrder.degree_eq_zero_iff_totalDegree_eq_zero, MonomialOrder.degree_eq_zero_iff, Nat.factorization_one, antidiagonal_zero, mapRange_eq_zero, MonomialOrder.toSyn_eq_zero_iff, toDFinsupp_smul, MultilinearMap.freeFinsuppEquiv_single, optionElim_zero, Representation.free_single_single, mapRange_zero, sum_uncurry_index, Module.Flat.iff_forall_exists_factorization, sigmaFinsuppEquivDFinsupp_single, Algebra.Generators.toComp_toAlgHom_monomial, Multiset.toFinsupp_zero, coe_eq_zero, MonomialOrder.degree_zero, Ordinal.CNF.coeff_zero_right, support_smul, instPosSMulMono, degree_preimage_nsmul, Module.Flat.exists_factorization_of_apply_eq_zero_of_free, embDomain_zero, KaehlerDifferential.kerTotal_mkQ_single_smul, MvPolynomial.constantCoeff_eq, MvPowerSeries.coeff_zero_C, Finset.finsuppAntidiag_empty_zero, MvPowerSeries.coeff_C, mapRange.zeroHom_comp, linearIndependent_iff, Finset.finsuppAntidiag_empty, instSMulPosStrictMono, List.support_sum_subset, Rep.leftRegularTensorTrivialIsoFree_inv_hom, sum_smul_index_semilinearMap', subtypeDomain_eq_zero_iff, graph_zero, MvPowerSeries.coeff_invOfUnit, uncurry_apply_pair, curryLinearEquiv_apply, mapRange.zeroHom_apply, MvPowerSeries.coeff_zero_X, default_eq_zero, Nat.factorization_eq_zero_iff', sigmaFinsuppEquivDFinsupp_apply, MvPolynomial.divMonomial_zero, curryEquiv_symm_apply, support_smul_eq, support_eq_empty, graph_eq_empty, MvPowerSeries.monomial_zero_one, toDFinsupp_zero, Rep.freeLift_hom, curryAddEquiv_symm_apply, SkewMonoidAlgebra.toFinsupp_eq_zero, degree_eq_zero_iff, Rep.freeLift_hom_single_single, Rep.leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single, sum_smul_index_addMonoidHom, mapRange.zeroHom_id, faithfulSMul, TensorProduct.sum_tmul_basis_left_eq_zero, sum_zero_index, Finset.finsuppAntidiag_zero, smul_single_one, Representation.free_asModule_free, cons_zero_zero, single_zero, MvPolynomial.isEmptyRingEquiv_eq_coeff_zero, single_nonneg, Rep.diagonalSuccIsoFree_hom_hom_single, TensorProduct.sum_tmul_basis_right_eq_zero, erase_single, Rep.free_ext_iff, List.toFinsupp_nil, smul_single, subtypeDomain_zero, Module.Presentation.tautologicalRelations_relation, finsuppProdLEquiv_symm_apply_apply, nsmul_single_one_image, isScalarTower, card_support_eq_zero, MvPolynomial.coeff_zero_one, Rep.leftRegularTensorTrivialIsoFree_hom_hom, weight_eq_zero_iff_eq_zero, support_curry, Rep.barComplex.d_single, mapDomain_smul, exteriorPower.presentation.relations_relation, MvPolynomial.coeff_expand_zero, Module.subsingletonEquiv_apply, coe_zero, MvPolynomial.support_C, Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single, DFinsupp.toFinsupp_zero, factorization_one, filter_zero, curryLinearEquiv_symm_apply, prod_zero_index, Rep.leftRegularTensorTrivialIsoFree_inv_hom_single_single, single_of_single_apply, curry_apply
|
mapRange 📖 | CompOp | 55 mathmath: range_mapRange, mapRange_apply, MvPolynomial.map_mapRange_eq_iff, floorDiv_def, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, mapRange_neg, mapDomain_mapRange, embDomain_mapRange, mapRange.addEquiv_apply, MonoidAlgebra.opRingEquiv_symm_apply, mapRange.addMonoidHom_apply, mapRange_neg', AddMonoidAlgebra.opRingEquiv_symm_apply, Algebra.TensorProduct.basis_repr_tmul, TensorProduct.equivFinsuppOfBasisRight_apply_tmul, mapRange_sub', TensorProduct.equivFinsuppOfBasisLeft_apply_tmul, mapRange_smul, MonoidAlgebra.coe_mapRangeRingHom, ceilDiv_def, mapRange.linearMap_apply, MvPolynomial.mapRange_eq_map, Algebra.TensorProduct.basisAux_tmul, mapRange_injective, mapRange_neLocus_eq, mapRange_add', mapRange_comp, support_mapRange, AddMonoidAlgebra.coe_mapRangeRingHom, mapRange_surjective, Polynomial.derivativeFinsupp_map, mapRange_smul', mapRange_sub, mapRange_id, mapRange_eq_zero, mapRange_zero, AddMonoidAlgebra.opRingEquiv_apply, mapRange.equiv_apply, mapRange.linearEquiv_apply, support_mapRange_of_injective, prod_mapRange_index, mapRange.zeroHom_apply, mapRange_add, MvPolynomial.coeff_mapRange, sum_mapRange_index, lmap_finsuppLEquivDirectSum_eq, mapRange_mapRange, mapRange_single, mapRange_finset_sum, Module.Basis.algebraMapCoeffs_repr, MonoidAlgebra.opRingEquiv_apply, mapRange_multiset_sum, subset_mapRange_neLocus, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply
|
ofSupportFinite 📖 | CompOp | 3 mathmath: ofSupportFinite_support, ofSupportFinite_fin_two_eq, ofSupportFinite_coe
|
onFinset 📖 | CompOp | 8 mathmath: onFinset_apply, support_onFinset, onFinset_prod, onFinset_sum, coe_onFinset, support_onFinset_subset, mem_support_onFinset, linearCombination_onFinset
|
onFinset_support 📖 | CompOp | 1 mathmath: Module.End.ringEquivEndFinsupp_apply_apply_support
|
support 📖 | CompOp | 235 mathmath: AddMonoidAlgebra.sup_support_list_prod_le, support_finset_sum, rangeSingleton_support, mem_support_iff, mem_supported_support, card_Ioc, MonoidAlgebra.support_one_subset, MvPolynomial.coeff_X_mul', ofSupportFinite_support, support_extendDomain_subset, card_Ico, if_mem_support, List.toFinsupp_support, support_single_add_single, support_zero, Algebra.FormallyUnramified.finite_of_free_aux, Equiv.finsuppUnique_symm_apply_support_val, neLocus_self_add_left, Finset.mem_finsuppAntidiag, mem_supported, comapDomain_smul_of_injective, sumElim_support, support_mul, mapDomain_support_of_injective, MonoidAlgebra.mem_adjoin_support, eq_single_iff, ext_iff', neLocus_eq_support_sub, notMem_support_iff, mapDomain_support, Multiset.support_sum_subset, fun_support_eq, MonoidAlgebra.support_gen_of_gen', MvPolynomial.mem_vars, Finset.support_sum_subset, disjoint_iff, support_onFinset, span_le_supported_biUnion_support, toDFinsupp_support, sum_ite_eq, SkewMonoidAlgebra.support_toFinsupp, BoundedContinuousFunction.mem_charPoly, BoundedContinuousFunction.charAlgHom_apply, QuadraticMap.map_finsuppSum, mapDomain_injOn, AddMonoidAlgebra.support_mul_single_subset, sum_ite_eq', Multiset.mem_sup_map_support_iff, Finset.mem_finsupp_iff, neLocus_zero_left, MonoidAlgebra.mem_span_support, AddMonoidAlgebra.le_inf_support_add, AddMonoidAlgebra.sup_support_multiset_prod_le, AddMonoidAlgebra.support_single_mul_subset, support_mul_subset_right, MvPolynomial.vars_monomial, MonoidAlgebra.support_mul_single_eq_image, degree_apply, AddMonoidAlgebra.le_inf_support_pow, MvPolynomial.vars_eq_support_biUnion_support, Nat.support_factorization, Polynomial.support_ofFinsupp, card_Icc, equivFunOnFinite_symm_apply_support, Polynomial.derivativeFinsupp_derivative, support_single_ne_zero, card_uIcc, MvPolynomial.finsupp_support_eq_support, card_Ioo, comapDomain_surjective, comapDomain_mapDomain, support_sum, HahnSeries.SummableFamily.coeff_support, sum_filter_index, filter_eq_sum, mem_toMultiset, support_erase, linearDepOn_iff, support_update_ne_zero, support_subset_singleton, Submodule.mem_span_set, Finset.mem_sup_support_iff, support_ceilDiv_subset, AddMonoidAlgebra.le_inf_support_list_prod, prod_eq_zero_iff, support_sym2Mul_subset, MvPolynomial.eval_eq, prod_filter_index, MonoidAlgebra.support_mul_single_subset, support_embSigma, card_support_le_one', support_eq_singleton, QuadraticMap.map_finsuppSum', AddMonoidAlgebra.support_mul_single_eq_image, AList.lookupFinsupp_support, Module.Basis.mem_span_image, support_update, AddMonoidAlgebra.exists_supDegree_mem_support, support_nonempty_iff, Prime.dvd_finsuppProd_iff, support_mapRange, neLocus_zero_right, AddMonoidAlgebra.support_mul, MvPolynomial.coeff_mul_X', MvPolynomial.prod_X_pow_eq_monomial, support_mono, multinomial_eq, neLocus_self_sub_left, List.mem_foldr_sup_support_iff, support_subtypeDomain, AddMonoidAlgebra.support_one_subset, supportedEquivFinsupp_symm_apply_coe_support_val, support_single_add_single_subset, finite_vaddAntidiagonal, support_floorDiv_subset, MonoidAlgebra.support_mul_single, AddMonoidAlgebra.sup_support_mul_le, MonoidAlgebra.support_gen_of_gen, PointedCone.mem_span_set, LaurentPolynomial.toLaurent_support, MonoidAlgebra.support_single_mul_eq_image, AddMonoidAlgebra.le_inf_support_mul, subset_support_tsub, AddMonoidAlgebra.mem_grade_iff, support_single_disjoint, AddMonoidAlgebra.mem_adjoin_support, support_smul, mem_support_single, support_update_subset, AddMonoidAlgebra.domCongr_support, union_support_maximal_linearIndependent_eq_range_basis, SkewMonoidAlgebra.support_ofFinsupp, MonoidAlgebra.support_single_mul, toFinset_toMultiset, card_support_eq_one', List.support_sum_subset, AddMonoidAlgebra.sup_support_pow_le, AddMonoidAlgebra.support_divOf, support_add, support_inf_union_support_sup, AddEquiv.finsuppUnique_symm_apply_support_val, DFinsupp.toFinsupp_support, support_onFinset_subset, prod_ite_eq, support_mapRange_of_injective, support_subset_singleton', card_Iic, card_Iio, restrictSupportEquiv_symm_single, AddMonoidAlgebra.sup_support_add_le, cons_support, Module.Basis.repr_support_subset_of_mem_span, supportedEquivFinsupp_apply_support_val, AddMonoidAlgebra.support_single_mul, mem_support_onFinset, extendDomain_support, support_neg, AddMonoidAlgebra.support_single_mul_eq_image, LaurentPolynomial.support_C_mul_T_of_ne_zero, image_fst_graph, MvPolynomial.support_esymm'', restrictSupportEquiv_apply, smul_apply_addAction, piecewise_support, linearDepOn_iffₛ, Icc_eq, support_smul_eq, Polynomial.support_derivativeFinsupp_subset_range, MvPolynomial.eval₂_eq, support_eq_empty, rangeIcc_support, QuadraticMap.apply_linearCombination, support_mul_subset_left, Polynomial.support_toFinsupp, support_single_subset, support_update_zero, AddMonoidAlgebra.support_gen_of_gen, MvPolynomial.mem_degrees, Module.End.ringEquivEndFinsupp_apply_apply_support, AddMonoidAlgebra.mem_span_support', MonoidAlgebra.domCongr_support, Nat.prod_primeFactors_invOn_squarefree, mem_support_toFun, AddMonoidAlgebra.sup_support_finset_prod_le, support_sup, support_subset_iff, neLocus_self_add_right, support_monotone, support_embDomain, LaurentPolynomial.support_C_mul_T, Submodule.mem_span_set_iff_exists_finsupp_le_finrank, support_sup_union_support_inf, QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar, card_support_le_one, Submodule.mem_set_smul, AddMonoidAlgebra.le_inf_support_finset_prod, comapDomain_add_of_injective, support_inf, Finset.mem_finsuppAntidiag', AddMonoidAlgebra.le_inf_support_multiset_prod, MonoidAlgebra.support_single_mul_subset, support_indicator_subset, support_tsub, HahnSeries.SummableFamily.support_powerSeriesFamily_subset, support_filter, HahnSeries.SummableFamily.coeff_hsum_eq_sum, Module.Basis.mem_span_repr_support, AddMonoidAlgebra.support_gen_of_gen', supportedEquivFinsupp_apply_apply, nsmul_single_one_image, neLocus_self_sub_right, MonoidAlgebra.support_mul, sigma_support, mem_sym2_support_of_mul_ne_zero, card_support_eq_zero, Multiset.toFinsupp_support, support_curry, support_zipWith, prod_ite_eq', restrictSupportEquiv_symm_apply_coe, support_eq_singleton', support_factorization, MonoidAlgebra.support_one, AddMonoidAlgebra.mem_gradeBy_iff, degree_def, toAList_keys_toFinset, AddMonoidAlgebra.mem_span_support, AddMonoidAlgebra.support_mul_single, MvPolynomial.bind₁_monomial, AddMonoidAlgebra.supDegree_mem_support, card_support_eq_one, support_sub, AddMonoidAlgebra.support_one, image_pow_eq_finsuppProd_image, sym2_support_eq_preimage_support_mul
|
toFun 📖 | CompOp | 2 mathmath: coe_strictMono, coe_mono
|
zipWith 📖 | CompOp | 5 mathmath: zipWith_apply, zipWith_neLocus_eq_left, zipWith_neLocus_eq_right, zipWith_single_single, support_zipWith
|