| Metric | Count |
|---|
DefinitionsC, X, coeff, coeffAddMonoidHom, coeffs, coeffsIn, constantCoeff, lcoeff, monomial, monomialOneHom, support | 11 |
Theoremsmonomial, C_0, C_1, C_add, C_apply, C_dvd_iff_dvd_coeff, C_eq_coe_nat, C_eq_smul_one, C_eq_zero, C_inj, C_injective, C_mem_coeffsIn, C_mul, C_mul', C_mul_X_eq_monomial, C_mul_X_pow_eq_monomial, C_mul_monomial, C_ne_zero, C_pow, C_surjective, X_inj, X_injective, X_mul_cancel_left_iff, X_mul_cancel_right_iff, X_mul_mem_coeffsIn, X_ne_zero, X_pow_eq_monomial, adjoin_range_X, algHom_C, algHom_ext, algHom_ext', algHom_ext'_iff, algHom_ext_iff, algebraMap_apply, algebraMap_eq, as_sum, coe_coeffsIn, coeffAddMonoidHom_apply, coeff_C, coeff_C_mul, coeff_X, coeff_X', coeff_X_mul, coeff_X_mul', coeff_X_pow, coeff_add, coeff_mapRange, coeff_mem_coeffs, coeff_monomial, coeff_monomial_mul, coeff_monomial_mul', coeff_mul, coeff_mul_X, coeff_mul_X', coeff_mul_monomial, coeff_mul_monomial', coeff_one, coeff_prod_X_pow, coeff_single_X, coeff_single_X_pow, coeff_smul, coeff_sum, coeff_zero, coeff_zero_C, coeff_zero_X, coeff_zero_one, coeffsIn_eq_span_monomial, coeffsIn_le, coeffsIn_mul, coeffsIn_pow, coeffs_C, coeffs_C_subset, coeffs_X_mul, coeffs_add, coeffs_eq_empty_of_subsingleton, coeffs_mul_X, coeffs_one, coeffs_one_of_nontrivial, coeffs_zero, constantCoeff_C, constantCoeff_X, constantCoeff_comp_C, constantCoeff_comp_algebraMap, constantCoeff_eq, constantCoeff_monomial, constantCoeff_smul, disjoint_support_monomial, eq_C_of_isEmpty, eq_zero_iff, exists_coeff_ne_zero, ext, ext_iff, finsupp_support_eq_support, hom_eq_hom, induction_on, induction_on', induction_on'', induction_on_monomial, infinite_of_infinite, infinite_of_nonempty, instIsCancelMulZeroOfIsCancelAdd, instIsDomainOfIsCancelAdd, instNoZeroDivisors, isRegular_X, isRegular_X_pow, isRegular_prod_X, is_id, lcoeff_apply, le_coeffsIn_pow, linearMap_ext, linearMap_ext_iff, mem_coeffsIn, mem_coeffsIn_iff_coeffs_subset, mem_coeffs_iff, mem_support_iff, monic_monomial_eq, monomialOneHom_apply, monomial_add_induction_on, monomial_add_single, monomial_eq, monomial_eq_monomial_iff, monomial_eq_zero, monomial_finsupp_sum_index, monomial_left_inj, monomial_left_injective, monomial_mem_coeffsIn, monomial_mul, monomial_mul_mem_coeffsIn, monomial_one_mul_cancel_left_iff, monomial_one_mul_cancel_right_iff, monomial_pow, monomial_single_add, monomial_sum_index, monomial_sum_one, monomial_zero, monomial_zero', mul_X_mem_coeffsIn, mul_def, mul_monomial_mem_coeffsIn, ne_zero_iff, nontrivial_of_nontrivial, notMem_support_iff, one_coeffsIn, one_def, prod_X_pow, prod_X_pow_eq_monomial, ringHom_ext, ringHom_ext', ringHom_ext'_iff, single_eq_monomial, smul_eq_C_mul, smul_monomial, sum_C, sum_def, sum_monomial_eq, support_C, support_X, support_X_mul, support_X_pow, support_add, support_eq_empty, support_monomial, support_monomial_subset, support_mul, support_mul_X, support_nonempty, support_one, support_sdiff_support_subset_support_add, support_smul, support_smul_eq, support_sum, support_sum_monomial_coeff, support_symmDiff_support_subset_support_add, support_zero, zero_notMem_coeffs | 175 |
| Total | 186 |
| Name | Category | Theorems |
|---|
C š | CompOp | 223 mathmath: coe_C, map_comp_C, MonomialOrder.monic_X_sub_C, hom_C, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv, isOpenMap_comap_C, ker_map, optionEquivLeft_C, Algebra.Generators.toAlgHom_ofComp_localizationAway, pUnitAlgEquiv_symm_apply, Algebra.Presentation.localizationAway_relation, monomial_finsupp_sum_index, bindā_comp_C, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C, image_comap_C_basicOpen, degreeOf_C, bindā_C_left, iterToSum_C_X, map_evalā, evalāHom_C_id_eq_joinā, optionEquivRight_C, map_mvPolynomial_eq_evalā, aevalTower_comp_C, evalāHom_C_eq_bindā, constantCoeff_C, MvPowerSeries.trunc_C, weightedHomogeneousComponent_zero, esymmAlgHomMonomial_single, homogeneousComponent_C_mul, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc, killCompl_C, Algebra.Generators.H1Cotangent.Ī“Aux_C, Algebra.Generators.ofComp_val, expand_C, MonomialOrder.eq_C_of_degree_eq_zero, coeffs_C, optionEquivRight_X_none, WeierstrassCurve.Jacobian.polynomialY_eq, C_apply, ChevalleyThm.chevalley_mvPolynomialC, coeff_C, xInTermsOfW_eq, ACounit_C, degrees_C, C_mul_X_eq_monomial, Algebra.Presentation.comp_aeval_relation_inl, C_0, totalDegree_C, WeierstrassCurve.Projective.polynomialZ_eq, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C', coeff_C_mul, quotient_map_C_eq_zero, C_mul_monomial, commAlgEquiv_C, coeff_zero_C, MonomialOrder.monic_X_add_C, commAlgEquiv_X, C_1, wittPolynomial_one, evalā_C, IsLocalization.Away.mvPolynomialQuotientEquiv_apply, C_add, isHomogeneous_C_mul_X, rename_evalā, Algebra.Generators.localizationAway_Ļ, tensorEquivSum_one_tmul_C, algebraMap_apply, MvPowerSeries.truncFinset_C, C_surjective, isEmptyRingEquiv_symm_apply, bindā_C_right, MonomialOrder.degree_X_sub_C, aevalTower_C, xInTermsOfW_aux, totalDegree_eq_zero_iff_eq_C, Polynomial.Bivariate.equivMvPolynomial_symm_C, combinatorial_nullstellensatz_exists_linearCombination, wittStructureRat_rec, expand_eq_C, isUnit_iff_eq_C_of_isReduced, MonomialOrder.degree_C, vars_C_mul, Algebra.Generators.toAlgHom_ofComp_rename, wittStructureRat_rec_aux, Algebra.Generators.ker_localizationAway, algHom_C, leadingCoeff_toLex_C, derivation_C, dvd_smul_X_iff_exists, mem_map_C_iff, prime_C_iff, universalFactorizationMapPresentation_relation, MonomialOrder.monic_C_one, eq_C_of_isEmpty, WeierstrassCurve.Projective.polynomialX_eq, monomial_zero', Polynomial.homogenize_C_mul, WeierstrassCurve.Projective.polynomialY_eq, C_eq_zero, supDegree_toLex_C, WittVector.frobeniusPolyAux_eq, C_mul', Algebra.Generators.cMulXSubOneCotangent_eq, map_C, C_dvd_iff_dvd_coeff, pderiv_C_mul, AlgebraicGeometry.AffineSpace.SpecIso_inv_over_assoc, quotient_mk_comp_C_isIntegral_of_isJacobsonRing, Algebra.Generators.Hom.toAlgHom_C, comap_C_surjective, finSuccEquiv_comp_C_eq_C, esymmAlgHom_zero, evalā_eta, WeierstrassCurve.Jacobian.polynomialZ_eq, finSuccEquiv_eq, RingHom.IsStandardSmooth.exists_etale_mvPolynomial, homogeneousComponent_zero, ker_evalāHom_universalFactorizationMap, monomial_sum_index, MonomialOrder.degree_eq_zero_iff, isEmptyRingEquiv_symm_toRingHom, MonomialOrder.leadingTerm_C, quotientEquivQuotientMvPolynomial_leftInverse, quotient_mk_comp_C_injective, dvd_X_iff_exists, MonomialOrder.leadingCoeff_C, ker_mapAlgHom, bindā_C_right, mkDerivationā_C, evalā_map_comp_C, optionEquivRight_apply, finSuccEquiv_apply, C_eq_coe_nat, degreeOf_mul_C_le, isHomogeneous_C_mul_X_pow, tensorEquivSum_C_tmul_one, degreeOf_C_mul_le, sumToIter_Xr, algebraMap_eq, sum_C, monomial_eq, vars_C, rename_prod_mk_evalā, aeval_C, rename_C, evalā_mul_C, C_neg, constantCoeff_comp_C, weightedHomogeneousComponent_C_mul, dvd_C_iff_exists, C_mem_pow_idealOfVars_iff, WeierstrassCurve.Jacobian.polynomialX_eq, aeval_C_comp_left, C_mul_X_pow_eq_monomial, eval_C, IsWeightedHomogeneous.C_mul, mapAlgHom_apply, isLocalization_C_mk', degreeOf_C_mul, C_injective, C_mul, CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_fst, isLocalization, IsSymmetric.C, ringHom_ext'_iff, smul_eq_C_mul, counitNat_C, derivation_C_mul, aeval_sumElim_pderiv_inl, iterToSum_C_C, totalDegree_sub_C_le, evalā_C_mk_eq_zero, coe_expand, aeval_sumElim, universalFactorizationMapPresentation_Ļ', isHomogeneous_C, Polynomial.homogenize_C, AlgebraicGeometry.AffineSpace.SpecIso_inv_over, counit_C, MonomialOrder.degree_X_add_C, C_mem_coeffsIn, evalāHom_C_left, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, Algebra.PreSubmersivePresentation.localizationAway_jacobiMatrix, C_pow, coeffs_C_subset, comp_C_integral_of_surjective_of_isJacobsonRing, C_sub, quotientEquivQuotientMvPolynomial_rightInverse, pderiv_C, C_dvd_iff_zmod, MvPowerSeries.trunc_C_mul, evalāHom_C, sumToIter_C, RingHom.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, supportedEquivMvPolynomial_symm_C, C_inj, IsHomogeneous.C_mul, optionEquivLeft_symm_C_C, C_p_pow_dvd_bindā_rename_wittPolynomial_sub_sum, MonomialOrder.C_mul_leadingCoeff_monomial_degree, tensorEquivSum_C_tmul_C, DividedPowerAlgebra.mkRingHom_C, evalā_assoc, instIsLocalHomRingHomC, Polynomial.Bivariate.equivMvPolynomial_C_C, DividedPowerAlgebra.mkAlgHom_C, isWeightedHomogeneous_C, eval_assoc, wittPolynomial_eq_sum_C_mul_X_pow, hom_bindā, C_dvd_iff_map_hom_eq_zero, support_C, bindā_monomial, mem_image_comap_C_basicOpen, C_eq_smul_one, Polynomial.toMvPolynomial_C, MvPowerSeries.trunc'_C, Algebra.Generators.C_mul_X_sub_one_mem_ker, MvPowerSeries.trunc'_C_mul, commAlgEquiv_C_X, expand_zero_apply, evalāHom_comp_C
|
X š | CompOp | 276 mathmath: KaehlerDifferential.mvPolynomialBasis_apply, vars_X, algHom_ext_iff, mul_X_divMonomial, CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_snd, aeval_X_left, evalāHom_X, MonomialOrder.monic_X_sub_C, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv, coeff_X_mul', expand_X, Algebra.Generators.cotangentSpaceBasis_apply, X_pow_eq_monomial, KaehlerDifferential.mvPolynomialBasis_repr_D_X, MonomialOrder.degree_X, Algebra.Generators.toAlgHom_ofComp_localizationAway, leibniz_iff_X, optionEquivLeft_X_some, aeval_X_left_apply, Polynomial.toPowerSeries_toMvPowerSeries, pUnitAlgEquiv_symm_apply, Algebra.Presentation.localizationAway_relation, coeffs_mul_X, StandardEtalePresentation.toPresentation_algebra_smul, totalDegree_X_pow, algHom_ext'_iff, aeval_X, scalarRTensor_apply_X_tmul_apply, irreducible_mul_X_add, optionEquivLeft_apply, ACounit_X, bindā_xInTermsOfW_wittPolynomial, iterToSum_C_X, supportedEquivMvPolynomial_symm_X, mkDerivation_X, Matrix.toMvPolynomial_one, supported_eq_adjoin_X, aeval_ite_mem_eq_self, map_mvPolynomial_eq_evalā, X_mul_cancel_right_iff, X_prime, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, bindā_X_left, Algebra.Generators.ofComp_val, X_mul_pderiv_monomial, X_injective, Algebra.Generators.naive_val, Algebra.Generators.toComp_val, Algebra.Generators.Hom.id_val, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, optionEquivRight_X_none, WeierstrassCurve.Jacobian.polynomialY_eq, coe_X, adjoin_range_X, mul_X_mem_coeffsIn, X_dvd_X, transcendental_polynomial_aeval_X_iff, coeff_X, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, X_mul_mem_coeffsIn, xInTermsOfW_eq, transcendental_supported_X_iff, optionEquivLeft_X_none, algebraicIndependent_polynomial_aeval_X, optionEquivRight_symm_apply, C_mul_X_eq_monomial, Algebra.Presentation.comp_aeval_relation_inl, WeierstrassCurve.Projective.polynomialZ_eq, evalā_X, X_dvd_monomial, iterToSum_X, coeff_X_pow, MonomialOrder.monic_X_add_C, aevalTower_X, commAlgEquiv_X, optionEquivRight_X_some, evalāHom_X', rTensor_apply_X_tmul, wittPolynomial_one, pderiv_X, IsLocalization.Away.mvPolynomialQuotientEquiv_apply, isHomogeneous_C_mul_X, WittVector.mul_polyOfInterest_aux4, coeff_sum_X_pow_of_fintype, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some, Algebra.Generators.localizationAway_Ļ, Polynomial.Bivariate.equivMvPolynomial_symm_X_0, WittVector.frobeniusPoly_zmod, X_mul_cancel_left_iff, X_dvd_mul_iff, degrees_X, IsWeightedHomogeneous.sum_weight_X_mul_pderiv, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord, coeff_single_X, Polynomial.toTupleMvPolynomial_one_eq, coeff_single_X_pow, dvd_X_mul_iff, MonomialOrder.degree_X_sub_C, xInTermsOfW_aux, Algebra.Generators.Hom.toAlgHom_X, degreeOf_mul_X_eq_degreeOf_add_one_iff, Polynomial.homogenize_X_pow, combinatorial_nullstellensatz_exists_linearCombination, isRegular_prod_X, algebraTensorAlgEquiv_symm_X, coeff_prod_X_pow, mk_eq_evalā, monomial_add_single, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none, isHomogeneous_X, coeff_zero_X, Polynomial.Bivariate.equivMvPolynomial_symm_X_1, Algebra.Generators.ker_localizationAway, support_mul_X, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, mkā_eq_aeval, dvd_smul_X_iff_exists, Algebra.Generators.comp_localizationAway_ker, universalFactorizationMapPresentation_relation, degreeOf_mul_X_self, WeierstrassCurve.Projective.polynomialX_eq, Matrix.mvPolynomialX_apply, Algebra.Generators.self_Ļ, modMonomial_X, WeierstrassCurve.Projective.polynomialY_eq, SymmetricAlgebra.equivMvPolynomial_symm_X, coeff_linearCombination_X_pow, linearIndependent_X, coeff_mul_X', prod_X_pow_eq_monomial, coeff_mul_X, universalFactorizationMapPresentation_algebra_algebraMap, xInTermsOfW_zero, constantCoeff_X, WittVector.frobeniusPolyAux_eq, bindā_X_right, Algebra.Generators.cMulXSubOneCotangent_eq, Polynomial.Bivariate.equivMvPolynomial_X, X_inj, Algebra.Generators.toKaehler_tmul_D, psum_one, X_dvd_iff_modMonomial_eq_zero, X_mul_divMonomial, evalā_eta, Algebra.Generators.toExtendScalars_val, WeierstrassCurve.Jacobian.polynomialZ_eq, isRegular_X, finSuccEquiv_eq, SymmetricAlgebra.equivMvPolynomial_Ī¹_apply, ker_evalāHom_universalFactorizationMap, monic_monomial_eq, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, Polynomial.Bivariate.equivMvPolynomial_C_X, quotientEquivQuotientMvPolynomial_leftInverse, support_X_pow, pderiv_X_of_ne, prod_X_add_C_coeff, isRegular_X_pow, AlgebraicClosure.Monics.map_eq_prod, Algebra.Generators.H1Cotangent.Ī“Aux_X, X_mul_modMonomial, dvd_X_iff_exists, finSuccEquiv_X_succ, degreeOf_X, X_mem_supported, hsymm_one, coeff_X', totalDegree_X, StandardEtalePresentation.toPresentation_Ļ', evalāHom_eq_bindā, prod_C_add_X_eq_sum_esymm, optionEquivRight_apply, finSuccEquiv_apply, tensorEquivSum_X_tmul_X, Algebra.Presentation.relation_comp_localizationAway_inl, aeval_unique, DividedPowerAlgebra.dp_def, rename_polynomial_aeval_X, Algebra.Generators.Hom.equivAlgHom_symm_apply_val, isHomogeneous_C_mul_X_pow, Polynomial.toMvPolynomial_X, sumToIter_Xr, algebraicIndependent_X, monomial_eq, IsTranscendenceBasis.mvPolynomial, transcendental_polynomial_aeval_X, WittVector.wittMul_zero, evalā_X_pow, WittVector.polyOfInterest_vars_eq, pderiv_inr_universalFactorizationMap_X, MonomialOrder.leadingCoeff_X, WittVector.wittNeg_zero, WeierstrassCurve.Jacobian.polynomialX_eq, transcendental_X, msymm_one, C_mul_X_pow_eq_monomial, mapAlgHom_apply, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, optionEquivLeft_symm_apply, homogeneousSubmodule_one_eq_span_X, evalāHom_id_X_eq_joinā, esymm_eq_multiset_esymm, comap_apply, IsTranscendenceBasis.mvPolynomial', StandardEtalePresentation.toPresentation_val, rename_X, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, ringHom_ext'_iff, divMonomial_add_modMonomial_single, degrees_X', prod_X_pow, universalFactorizationMapPresentation_algebra_smul, IsHomogeneous.sum_X_mul_pderiv, aeval_sumElim_pderiv_inl, tensorEquivSum_one_tmul_X, coeff_X_mul, mkDerivationā_X, evalā_C_mk_eq_zero, universalFactorizationMapPresentation_val, coe_expand, aeval_sumElim, KaehlerDifferential.mvPolynomialBasis_repr_symm_single, wittPolynomial_zero, coeff_linearCombination_X_pow_of_fintype, bindā_wittPolynomial_xInTermsOfW, Polynomial.homogenize_C, evalāAlgHom_X, counitNat_X, MonomialOrder.degree_X_add_C, optionEquivLeft_symm_C_X, mul_X_modMonomial, Polynomial.homogenize_X, finSuccEquiv_X_zero, bindā_X_right, transcendental_supported_polynomial_aeval_X_iff, StandardEtalePresentation.toPresentation_relation, Algebra.PreSubmersivePresentation.ofHasCoeffs_val, esymm_eq_sum_subtype, pderiv_X_self, quotientEquivQuotientMvPolynomial_rightInverse, WittVector.mul_polyOfInterest_aux3, modMonomial_add_divMonomial_single, isWeightedHomogeneous_X, esymm_one, optionEquivLeft_symm_X, SymmetricAlgebra.IsSymmetricAlgebra.mvPolynomial, X_divMonomial, tensorEquivSum_X_tmul_one, eval_X, transcendental_supported_X, degreeOf_mul_X_of_ne, WittVector.wittSub_zero, support_X, coeff_add_pow, map_X, monomial_single_add, wittPolynomial_eq_sum_C_mul_X_pow, LinearMap.toMvPolynomial_id, Polynomial.homogenize_one, support_X_mul, coeffs_X_mul, MonomialOrder.monic_X, derivation_ext_iff, WittVector.wittAdd_zero, mem_ideal_span_X_image, isHomogeneous_X_pow, esymmAlgEquiv_symm_apply, Algebra.Generators.C_mul_X_sub_one_mem_ker, DividedPowerAlgebra.dp_eq_mkRingHom, commAlgEquiv_C_X, Polynomial.coeff_freeMonic, MonomialOrder.degree_X_le_single, transcendental_supported_polynomial_aeval_X, sumToIter_Xl, pderiv_inl_universalFactorizationMap_X, counit_X
|
coeff š | CompOp | 115 mathmath: coeff_neg, map_mapRange_eq_iff, rTensor_apply_tmul_apply, coeff_divMonomial, sum_def, coeff_X_mul', image_comap_C_basicOpen, notMem_support_iff, weightedHomogeneousComponent_zero, MvPowerSeries.coeff_truncFinset_of_mem, coeff_expand_smul, MonomialOrder.coeff_eq_zero_of_lt, coeff_C, coeff_X, MvPowerSeries.coeff_trunc'_mul_trunc'_eq_coeff_mul, isUnit_iff_totalDegree_of_isReduced, coeff_homogeneousComponent, MonomialOrder.coeff_prod_sum_degree, coeff_rename_embDomain, isUnit_iff, finSuccEquiv_coeff_coeff, coeff_C_mul, coeff_X_pow, coeff_zero_C, IsNonarchimedean.eval_mvPolynomial_le, eval_eq', ext_iff, coeff_sum_X_pow_of_fintype, coeff_smul, coeff_monomial_mul, coeff_modMonomial_of_le, optionEquivLeft_coeff_coeff, mem_pow_idealOfVars_iff', coeff_single_X, coeff_single_X_pow, eq_zero_iff, MvPowerSeries.coeff_truncFinset_mul_truncFinset_eq_coeff_mul, totalDegree_eq_zero_iff_eq_C, coeff_sumSMulX, coeff_rename_mapDomain, coeff_prod_X_pow, eval_eq, as_sum, isNilpotent_iff, evalā_eq', coeff_coe, coeff_monomial_mul', MvPowerSeries.coeff_trunc', coeff_zero_X, coe_def, MvPowerSeries.coeff_trunc, mem_map_C_iff, IsHomogeneous.coeff_eq_zero, MonomialOrder.coeff_degree_eq_zero_iff, eq_C_of_isEmpty, coeff_one, homogeneousComponent_apply, coeff_linearCombination_X_pow, coeff_mul_X', coeff_mul_X, coeff_rTensorAlgHom_tmul, optionEquivLeft_coeff_some_coeff_none, mem_coeffsIn, coeff_mem_coeffs, C_dvd_iff_dvd_coeff, Height.mulHeightBound_eq, homogeneousComponent_zero, coeff_map, FirstOrder.Ring.MvPolynomialSupportLEEquiv_symm_apply_coeff, coeff_zero, coeff_modMonomial_of_not_le, coeff_X', MonomialOrder.coeff_pow_nsmul_degree, constantCoeff_eq, isIntegral_iff_isIntegral_coeff, coeff_rTensorAlgHom_monomial_tmul, support_sum_monomial_coeff, coeff_sub, coeff_expand_of_not_dvd, MvPowerSeries.coeff_mul_eq_coeff_trunc'_mul_trunc', coeff_add, Polynomial.coeff_homogenize, MvPowerSeries.coeff_truncFinset_eq_zero, MonomialOrder.Monic.coeff_degree, coeff_monomial, coeff_mul_monomial, evalā_eq, mem_ideal_span_monomial_image_iff_dvd, coeff_mapRange, coeffAddMonoidHom_apply, IsWeightedHomogeneous.coeff_eq_zero, coeff_X_mul, coeff_linearCombination_X_pow_of_fintype, MvPowerSeries.coeff_truncFinset, coeff_weightedHomogeneousComponent, MonomialOrder.coeff_mul_of_degree_add, MonomialOrder.coeff_sPolynomial_sup_eq_zero, coeff_rename_eq_zero, MonomialOrder.coeff_mul_of_add_of_degree_le, leadingCoeff_toLex, coeff_mul_monomial', lcoeff_apply, FirstOrder.Ring.mvPolynomial_zeroLocus_definable, isEmptyRingEquiv_eq_coeff_zero, mem_coeffs_iff, scalarRTensor_apply_tmul_apply, coeff_zero_one, coeff_add_pow, coeff_eq_zero_of_totalDegree_lt, coeff_expand_zero, weightedHomogeneousComponent_apply, coeff_mul, mem_image_comap_C_basicOpen, coeff_killCompl, coeff_sum
|
coeffAddMonoidHom š | CompOp | 1 mathmath: coeffAddMonoidHom_apply
|
coeffs š | CompOp | 19 mathmath: coeffs_add, coeffs_mul_X, mem_range_map_iff_coeffs_subset, coeffs_one, coeffs_one_of_nontrivial, coeffs_C, Algebra.Presentation.coeffs_relation_subset_coeffs, zero_notMem_coeffs, Algebra.Presentation.coeffs_relation_subset_core, coe_coeffs_map, coeff_mem_coeffs, mem_coeffsIn_iff_coeffs_subset, coeffs_map, coeffs_C_subset, mem_coeffs_iff, coeffs_eq_empty_of_subsingleton, coeffs_zero, Algebra.Presentation.HasCoeffs.coeffs_relation_mem_range, coeffs_X_mul
|
coeffsIn š | CompOp | 16 mathmath: monomial_mul_mem_coeffsIn, mul_X_mem_coeffsIn, X_mul_mem_coeffsIn, coeffsIn_mul, le_coeffsIn_pow, monomial_mem_coeffsIn, mem_coeffsIn, mem_coeffsIn_iff_coeffs_subset, coeffsIn_eq_span_monomial, coeffsIn_pow, mul_monomial_mem_coeffsIn, one_coeffsIn, range_mapAlgHom, C_mem_coeffsIn, coeffsIn_le, coe_coeffsIn
|
constantCoeff š | CompOp | 36 mathmath: eval_zero', constantCoeff_wittStructureRat, evalā_zero'_apply, constantCoeff_rename, constantCoeff_C, constantCoeff_wittStructureInt, evalāHom_zero_apply, evalāHom_zero', constantCoeff_smul, evalāHom_zero'_apply, eval_zero, evalā_zero_apply, constantCoeff_wittPolynomial, aeval_eq_constantCoeff_of_vars, constantCoeff_monomial, evalāHom_zero, aeval_zero, constantCoeff_X, WittVector.constantCoeff_wittMul, WittVector.constantCoeff_wittAdd, constantCoeff_wittStructureRat_zero, constantCoeff_eq, LinearMap.toMvPolynomial_constantCoeff, WittVector.constantCoeff_wittNSMul, constantCoeff_comp_C, WittVector.constantCoeff_wittZSMul, evalāHom_eq_constantCoeff_of_vars, aeval_zero', constantCoeff_xInTermsOfW, WittVector.constantCoeff_wittNeg, constantCoeff_comp_map, Matrix.toMvPolynomial_constantCoeff, constantCoeff_map, constantCoeff_wittStructureInt_zero, constantCoeff_comp_algebraMap, WittVector.constantCoeff_wittSub
|
lcoeff š | CompOp | 2 mathmath: rTensor_apply, lcoeff_apply
|
monomial š | CompOp | 140 mathmath: pUnitAlgEquiv_symm_monomial, dvd_monomial_one_iff_exists, MonomialOrder.sPolynomial_leadingTerm_mul', totalDegree_monomial, degrees_monomial, one_def, scalarRTensor_apply_monomial_tmul, MonomialOrder.degree_monomial, X_pow_eq_monomial, leibniz_iff_X, divMonomial_add_modMonomial, evalāHom_monomial, support_monomial, monomial_finsupp_sum_index, mul_def, smul_monomial, monomial_zero, monomial_eq_monomial_iff, evalā_mul_monomial, expand_monomial, monomial_mul_mem_coeffsIn, monomial_one_dvd_iff_modMonomial_eq_zero, X_mul_pderiv_monomial, coe_monomial, C_apply, single_eq_monomial, MonomialOrder.leadingTerm_monomial, MonomialOrder.span_leadingTerm_eq_span_monomial, MonomialOrder.span_leadingTerm_eq_span_monomialā, C_mul_X_eq_monomial, bindā_monomial, monomialOneHom_apply, monomial_left_inj, X_dvd_monomial, C_mul_monomial, Algebra.Generators.H1Cotangent.Ī“Aux_monomial, vars_monomial, pow_idealOfVars_eq_span, bindā_monomial_one, coeff_monomial_mul, dvd_monomial_iff_exists, mkDerivationā_monomial, killCompl_monomial_eq_zero_of_not_subset, modMonomial_add_divMonomial, MonomialOrder.span_leadingTerm_eq_span_monomial', monomial_one_mul_cancel_left_iff, coe_basisMonomials, monomial_mem_pow_idealOfVars_iff, MonomialOrder.monic_monomial, MonomialOrder.sPolynomial_def, killCompl_monomial_mapDomain, as_sum, MonomialOrder.leadingCoeff_monomial, monomial_add_single, MonomialOrder.monic_monomial_one, monomial_eq_zero, eval_monomial, coeff_monomial_mul', monomial_mem_coeffsIn, mkDerivation_monomial, rename_monomial, isWeightedHomogeneous_monomial, monomial_zero', MvPowerSeries.truncFinset_monomial, homogeneousComponent_apply, divMonomial_mul_monomial, prod_X_pow_eq_monomial, constantCoeff_monomial, divMonomial_monomial, isHomogeneous_monomial, map_monomial, monomial_mem_restrictSupport, MonomialOrder.sPolynomial_monomial_mul, monomial_left_injective, monomial_sum_index, monic_monomial_eq, pderiv_monomial_single, support_monomial_subset, monomial_mul, rTensor_symm_apply_single, pderiv_monomial, Algebra.Generators.toComp_toAlgHom_monomial, monomial_mem_homogeneousSubmodule_pow_degree, dvd_monomial_mul_iff_exists, rTensor_apply_monomial_tmul, coeff_rTensorAlgHom_monomial_tmul, support_sum_monomial_coeff, coeffsIn_eq_span_monomial, Algebra.Generators.ofComp_toAlgHom_monomial_sumElim, monomial_eq, esymm_eq_sum_monomial, totalDegree_monomial_le, mul_monomial_mem_coeffsIn, MonomialOrder.sPolynomial_monomial_mul', C_mul_X_pow_eq_monomial, optionEquivLeft_monomial, divMonomial_monomial_mul, sum_monomial_eq, degrees_monomial_eq, pUnitAlgEquiv_monomial, coeff_monomial, coeff_mul_monomial, mem_ideal_span_monomial_image_iff_dvd, IsRegular.monomial, monomial_pow, evalā_monomial, prod_X_pow, monomial_one_dvd_monomial_one, mul_monomial_modMonomial, Algebra.Generators.Hom.toAlgHom_monomial, monomial_sum_one, scalarRTensor_symm_apply_single, mem_ideal_span_monomial_image, disjoint_support_monomial, aeval_monomial, MonomialOrder.degree_monomial_le, coeff_mul_monomial', algebraTensorAlgEquiv_symm_monomial, restrictSupport_eq_span, killCompl_monomial_eq_monomial_comapDomain_of_subset, killCompl_monomial, coeffsIn_le, MonomialOrder.C_mul_leadingCoeff_monomial_degree, Algebra.Generators.comp_Ļ, MvPowerSeries.truncFinset_apply, linearMap_ext_iff, monomial_single_add, monomial_one_mul_cancel_right_iff, degreeOf_monomial_eq, weightedHomogeneousComponent_apply, bindā_monomial, induction_on_monomial, vars_monomial_single, killCompl_monomial_eq_zero_of_notMem_range, monomial_modMonomial, MonomialOrder.sPolynomial_mul_monomial, MonomialOrder.sPolynomial_leadingTerm_mul, Polynomial.homogenize_monomial, monomial_dvd_monomial, monomial_mul_modMonomial
|
monomialOneHom š | CompOp | 1 mathmath: monomialOneHom_apply
|
support š | CompOp | 73 mathmath: support_sum, support_mul, support_finSuccEquiv, sum_def, mem_image_support_coeff_finSuccEquiv, support_monomial, mem_support_iff, notMem_support_iff, support_sdiff_support_subset_support_add, totalDegree_eq, support_eq_empty, MonomialOrder.degree_mem_support_iff, degrees_def, mem_vars, support_killCompl, support_add, support_rename_of_injective, support_expand_subset, IsNonarchimedean.eval_mvPolynomial_le, eval_eq', vars_eq_support_biUnion_support, MonomialOrder.support_leadingTerm', finsupp_support_eq_support, support_coeff_finSuccEquiv, support_neg, eval_eq, as_sum, evalā_eq', MonomialOrder.support_leadingTerm, support_mul_X, support_esymm', mem_support_coeff_optionEquivLeft, schwartz_zippel_sup_sum, mem_restrictSupport_iff, homogeneousComponent_apply, support_map_of_injective, exists_mem_support_not_dvd_of_forall_totalDegree_le, mem_support_finSuccEquiv, Height.mulHeightBound_eq, degreeOf_eq_sup, image_support_finSuccEquiv, support_nonempty, support_expand, MonomialOrder.degree_mem_support, support_monomial_subset, FirstOrder.Ring.MvPolynomialSupportLEEquiv_symm_apply_coeff, support_X_pow, support_optionEquivLeft, support_one, support_smul_eq, support_sum_monomial_coeff, weightedDecomposition.decompose'_eq, support_map_subset, support_divMonomial, support_zero, mem_support_coeff_finSuccEquiv, support_sub, support_esymm'', MonomialOrder.notMem_support_of_degree_lt, evalā_eq, support_rename_killCompl_subset, MvPowerSeries.support_truncFinset_subset, disjoint_support_monomial, FirstOrder.Ring.mvPolynomial_zeroLocus_definable, support_symmDiff_support_subset_support_add, mem_coeffs_iff, support_esymm, support_smul, support_X, support_X_mul, support_C, weightedHomogeneousComponent_apply, decomposition.decompose'_eq
|