Basic

📁 Source: Mathlib/Algebra/MvPolynomial/Basic.lean

Statistics

Metric	Count
Definitions C, X, algebra, coeff, coeffAddMonoidHom, coeffs, coeffsIn, commSemiring, constantCoeff, decidableEqMvPolynomial, distribuMulAction, inhabited, lcoeff, monomial, monomialOneHom, smulZeroClass, support, unique	18
Theorems monomial, 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_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, faithfulSMul, 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, isCentralScalar, isRegular_X, isRegular_X_pow, isRegular_prod_X, isScalarTower, isScalarTower_right, 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_eq_monomial, ringHom_ext, ringHom_ext', ringHom_ext'_iff, single_eq_monomial, smulCommClass, smulCommClass_right, 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_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	178
Total	196

IsRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
monomial 📖	mathematical	IsRegular Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	MvPolynomial MvPolynomial.commSemiring DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule MvPolynomial.module LinearMap.instFunLike MvPolynomial.monomial	—	isLeftRegular_iff_isRegular MvPolynomial.ext left MvPolynomial.coeff_monomial_mul

MvPolynomial

Definitions

Name	Category	Theorems
C 📖	CompOp	219 math math: 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, 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, 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, coe_expand, aeval_sumElim, universalFactorizationMapPresentation_σ', isHomogeneous_C, Polynomial.homogenize_C, AlgebraicGeometry.AffineSpace.SpecIso_inv_over, counit_C, MonomialOrder.degree_X_add_C, MonomialOrder.monic_one, 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, eval₂_assoc, instIsLocalHomRingHomC, Polynomial.Bivariate.equivMvPolynomial_C_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	263 math math: 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, 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, 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, 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, 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, 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, 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, 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', 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, bind₁_wittPolynomial_xInTermsOfW, Polynomial.homogenize_C, 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, 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, commAlgEquiv_C_X, Polynomial.coeff_freeMonic, MonomialOrder.degree_X_le_single, transcendental_supported_polynomial_aeval_X, sumToIter_Xl, pderiv_inl_universalFactorizationMap_X, counit_X
algebra 📖	CompOp	607 math math: pUnitAlgEquiv_symm_monomial, join₁_rename, aeval_sum, WittVector.bind₁_frobeniusPoly_wittPolynomial, KaehlerDifferential.mvPolynomialBasis_apply, Algebra.PreSubmersivePresentation.jacobiMatrix_naive, algHom_ext_iff, map_bind₁, Algebra.Generators.aeval_val_surjective, wittPolynomial_zmod_self, aeval_X_left, pUnitAlgEquiv_apply, exists_finset_rename, support_finSuccEquiv, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, WittVector.aeval_verschiebung_poly', rTensorAlgEquiv_apply, Algebra.Presentation.naive_toGenerators, mem_image_support_coeff_finSuccEquiv, comapEquiv_symm_coe, eval₂_expand, universalFactorizationMap_comp_map, aeval_algebraMap_eq_zero_iff, Algebra.PreSubmersivePresentation.ofHasCoeffs_map, expand_X, algebraicIndependent_iff_ker_eq_bot, Algebra.Generators.cotangentSpaceBasis_apply, IsWeightedHomogeneous.pderiv, WittVector.ghostComponent_apply, aeval_wittPolynomial, KaehlerDifferential.mvPolynomialBasis_repr_D_X, optionEquivLeft_C, rename_rename, Algebra.Generators.toAlgHom_ofComp_localizationAway, MvPowerSeries.trunc'_expand_trunc', optionEquivLeft_X_some, aeval_X_left_apply, Polynomial.toPowerSeries_toMvPowerSeries, pUnitAlgEquiv_symm_apply, expand_eq_zero, weightedHomogeneousSubmodule_mul, Ideal.span_pow_eq_map_homogeneousSubmodule, natDegree_finSuccEquiv, StandardEtalePresentation.toPresentation_algebra_smul, Ideal.span_eq_map_homogeneousSubmodule, algHom_ext'_iff, IntermediateField.mem_adjoin_iff, AlgebraicIndependent.repr_ker, aeval_X, comapEquiv_coe, Polynomial.pUnitAlgEquiv_symm_toPowerSeries, AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, optionEquivLeft_apply, instIsScalarTower, totalDegree_coeff_finSuccEquiv_add_le, map_comp_rename, ACounit_X, prime_rename_iff, bind₁_xInTermsOfW_wittPolynomial, constantCoeff_rename, Algebra.PreSubmersivePresentation.jacobiMatrix_reindex, CommRingCat.free_map_coe, Algebra.FinitePresentation.mvPolynomial_of_finitePresentation, Algebra.SubmersivePresentation.ofSubsingleton_algebra_algebraMap, killCompl_comp_rename, supportedEquivMvPolynomial_symm_X, pderiv_one, mkDerivation_X, pderiv_mul, Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp, ACounit_surjective, supported_eq_adjoin_X, aeval_eq_eval, aeval_ite_mem_eq_self, eval₂Hom_C_id_eq_join₁, PolynomialLaw.exists_lift', PolynomialLaw.toFun_eq_rTensor_φ_toFun', comap_id, eval_rename_prod_mk, optionEquivRight_C, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_one_equivMvPolynomial, aevalTower_comp_C, rename_msymm, comap_comp_apply, eval₂Hom_C_eq_bind₁, Algebra.PreSubmersivePresentation.ofHasCoeffs_relation, degreeOf_coeff_finSuccEquiv, rename_id_apply, nonempty_support_finSuccEquiv, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, pderiv_rename, Algebra.Presentation.comp_relation_inr, AlgebraicIndependent.aeval_comp_repr, map_expand, map_aeval, map_frobenius_expand, renameEquiv_trans, expand_monomial, expand_char, map_rename, Algebra.PreSubmersivePresentation.ofHasCoeffs_σ', killCompl_C, eval₂_const_pUnitAlgEquiv_symm, eval_comp_toMvPolynomial, Algebra.Generators.map_toComp_ker, support_finSuccEquiv_nonempty, Algebra.Generators.Hom.toExtensionHom_toAlgHom_apply, bind₁_X_left, sumAlgEquiv_comp_rename_inr, aevalTower_toAlgHom, X_mul_pderiv_monomial, degree_optionEquivLeft, mapAlgHom_id, Algebra.Generators.naive_val, coeff_expand_smul, Algebra.Generators.algebraMap_apply, expand_C, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, optionEquivRight_X_none, rename_psum, Algebra.Generators.map_ofComp_ker, expand_zero, degreesLE_nsmul, totalDegree_rename_le, coe_mapEquivMonic_comp', Algebra.Presentation.naive_relation, Polynomial.toMvPolynomial_eq_rename_comp, Polynomial.aeval_homogenize_X_one, adjoin_range_X, MonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure, AddMonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure, transcendental_polynomial_aeval_X_iff, aeval_algebraMap_eq_zero_iff_of_injective, Algebra.Generators.algebraMap_eq, Algebra.SubmersivePresentation.ofSubsingleton_relation, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, support_rename_of_injective, Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial, comap_comp, eval_eq_eval_mv_eval', ACounit_C, transcendental_supported_X_iff, optionEquivLeft_X_none, algebraicIndependent_polynomial_aeval_X, degreeOf_rename_of_injective, degreesLE_add, exists_rename_eq_of_vars_subset_range, optionEquivRight_symm_apply, Algebra.Generators.Hom.aeval_val, Algebra.Presentation.comp_aeval_relation_inl, WittVector.mulN_coeff, pderiv_sumToIter, support_expand_subset, coeff_rename_embDomain, TensorProduct.toIntegralClosure_mvPolynomial_bijective, finSuccEquiv_coeff_coeff, rename_comp_expand, Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, Algebra.PreSubmersivePresentation.jacobiMatrix_apply, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C', rename_esymm, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply, Algebra.Generators.toAlgHom_ofComp_surjective, bind₁_comp_bind₁, commAlgEquiv_C, Algebra.Generators.Hom.algebraMap_toAlgHom', Algebra.Generators.cotangentSpaceBasis_repr_tmul, aevalTower_X, commAlgEquiv_X, optionEquivRight_X_some, aeval_expand, AlgebraicIndependent.lift_reprField, aeval_algebraMap_apply, Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation, pderiv_X, Algebra.Generators.H1Cotangent.δAux_toAlgHom, Subalgebra.mvPolynomial_aeval_coe, IsLocalization.Away.mvPolynomialQuotientEquiv_apply, Algebra.Presentation.naive_relation_apply, PolynomialLaw.exists_lift, WittVector.mul_polyOfInterest_aux4, rename_eval₂, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some, MvPowerSeries.expand_eq_expand, mapAlgEquiv_apply, Polynomial.Bivariate.equivMvPolynomial_symm_X_0, algebraTensorAlgEquiv_symm_comp_aeval, finitePresentation_universalFactorizationMap, mapAlgEquiv_refl, Algebra.FiniteType.iff_quotient_mvPolynomial', tensorEquivSum_one_tmul_C, Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom, eval₂Hom_rename, sumAlgEquiv_comp_rename_inl, aeval_bind₁, algebraMap_apply, exists_fin_rename, optionEquivLeft_coeff_coeff, IsWeightedHomogeneous.sum_weight_X_mul_pderiv, Matrix.charpoly.optionEquivLeft_symm_univ_isHomogeneous, pderiv_def, mem_supported, renameEquiv_apply, rename_esymmAlgHom, aeval_eq_zero, eval₂_cast_comp, Algebra.PreSubmersivePresentation.naive_toPresentation, bind₁_C_right, instIsLocalHomRingHomAlgebraMap, WittVector.bind₁_wittMulN_wittPolynomial, PolynomialLaw.exists_range_φ_eq_of_fg, Algebra.FinitePresentation.mvPolynomial, aevalTower_C, expand_one_apply, map_expand_pow_char, MonomialOrder.degree_smul_le, AnalyticOnNhd.aeval_mvPolynomial, Algebra.Generators.Hom.toAlgHom_X, bind₁_rename, wittStructureRat_prop, degrees_rename, Algebra.Presentation.comp_relation, Polynomial.Bivariate.equivMvPolynomial_symm_C, Algebra.Generators.instIsScalarTowerRing, MvPowerSeries.aeval_coe, WittVector.IsPoly.poly, finite_universalFactorizationMap, rTensorAlgHom_toLinearMap, wittStructureRat_rec, expand_eq_C, MvPowerSeries.trunc'_expand, universalFactorizationMapPresentation_map, coeff_rename_mapDomain, algebraTensorAlgEquiv_symm_X, expand_injective, support_coeff_finSuccEquiv, Algebra.Presentation.aeval_val_relation, expand_one, esymmAlgHom_fin_surjective, expand_inj, coeffsIn_mul, Algebra.Generators.H1Cotangent.δAux_ofComp, le_coeffsIn_pow, supported_strictMono, exists_integral_inj_algHom_of_quotient, exists_finite_inj_algHom_of_fg, aeval_def, Algebra.Generators.toAlgHom_ofComp_rename, wittStructureRat_rec_aux, Polynomial.Bivariate.equivMvPolynomial_symm_X_1, supported_mono, MonomialOrder.sPolynomial_decomposition, totalDegree_expand, algHom_C, wittStructureInt_prop, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, derivation_C, mem_support_coeff_optionEquivLeft, dvd_smul_X_iff_exists, mem_supported_vars, mkDerivation_monomial, Algebra.Generators.Hom.toExtensionHom_toRingHom, Algebra.Generators.comp_localizationAway_ker, rename_monomial, aeval_toMvPolynomial, restrictScalars_restrictSupportIdeal, universalFactorizationMapPresentation_relation, aevalTower_comp_algebraMap, Algebra.PreSubmersivePresentation.aevalDifferential_single, AlgebraicIndependent.algebraMap_aevalEquiv, aeval_id_rename, Algebra.adjoin_range_eq_range_aeval, Algebra.Generators.aeval_val_σ, mem_zeroLocus_iff, totalDegree_coeff_optionEquivLeft_add_le, aeval_eq_constantCoeff_of_vars, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul, SymmetricAlgebra.equivMvPolynomial_symm_X, expand_bind₁, smul_eval, MvPowerSeries.substAlgHom_coe, universalFactorizationMapPresentation_algebra_algebraMap, coeff_rTensorAlgHom_tmul, aeval_zero, killCompl_rename_app, comp_aeval, frobenius_zmod, KaehlerDifferential.mvPolynomialBasis_repr_apply, optionEquivLeft_coeff_some_coeff_none, IntermediateField.mem_adjoin_range_iff, WittVector.coeff_frobeniusFun, renameEquiv_refl, totalDegree_renameEquiv, expand_mul, Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul, isLocalHom_expand, Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, C_mul', isEmptyAlgEquiv_apply, Polynomial.Bivariate.equivMvPolynomial_X, pderiv_C_mul, Module.Basis.symmetricAlgebra_repr_apply, MonomialOrder.degree_smul_of_isRegular, AlgebraicClosure.toSplittingField_coeff, natDegree_optionEquivLeft, Algebra.Generators.self_algebra_smul, restrictSupport_nsmul, Algebra.Generators.toKaehler_tmul_D, mem_support_finSuccEquiv, algebraicIndependent_iff_injective_aeval, aeval_map_algebraMap, Algebra.Generators.Hom.toAlgHom_C, rename_comp_toMvPolynomial, finSuccEquiv_comp_C_eq_C, coeToMvPowerSeries.algHom_apply, AlgebraicIndependent.liftAlgHom_comp_reprField, rename_rightInverse, finSuccEquiv_eq, SymmetricAlgebra.equivMvPolynomial_ι_apply, LinearMap.polyCharpoly_eq_of_basis, ker_eval₂Hom_universalFactorizationMap, bind₁_comp_rename, LinearMap.polyCharpolyAux_map_aeval, image_support_finSuccEquiv, pderiv_monomial_single, eval₂_rename, AlgebraicIndependent.aeval_repr, support_expand, Polynomial.Bivariate.equivMvPolynomial_C_X, IsSymmetric.rename, IsHomogeneous.aeval, aeval_bind₂, rename_bind₁, pderiv_X_of_ne, renameSymmetricSubalgebra_symm_apply_coe, Algebra.Generators.Hom.toAlgHom_comp_apply, degree_finSuccEquiv, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, nonempty_support_optionEquivLeft, pderiv_monomial, bind₁_rename_expand_wittPolynomial, Algebra.adjoin_eq_range, mapAlgEquiv_symm, Algebra.Generators.toComp_toAlgHom_monomial, rename_injective, monomial_mem_homogeneousSubmodule_pow_degree, Algebra.SubmersivePresentation.aeval_jacobianOfHasCoeffs, coe_smul, killCompl_map, Algebra.FiniteType.iff_quotient_mvPolynomial, aeval_eq_bind₁, support_optionEquivLeft, dvd_X_iff_exists, finSuccEquiv_X_succ, aeval_ofNat, Algebra.Presentation.aeval_val_relationOfHasCoeffs, expand_comp_bind₁, mapAlgEquiv_trans, Algebra.SubmersivePresentation.aeval_invJacobianOfHasCoeffs, ker_mapAlgHom, aeval_injective_iff_of_isEmpty, Algebra.Generators.ofComp_kerCompPreimage, X_mem_supported, esymmAlgHom_fin_injective, aeval_comp_bind₁, eval₂_const_pUnitAlgEquiv, Algebra.Generators.repr_CotangentSpaceMap, pderiv_pow, aeval_esymm_eq_multiset_esymm, supported_le_supported_iff, eval_rename, StandardEtalePresentation.toPresentation_σ', witt_structure_prop, LinearMap.toMvPolynomial_comp, IsHomogeneous.rename_isHomogeneous_iff, vars_bind₁, WittVector.bind₁_verschiebungPoly_wittPolynomial, Algebra.Presentation.instFinitePresentationModelOfHasCoeffsOfFinite, optionEquivRight_apply, finSuccEquiv_apply, tensorEquivSum_X_tmul_X, comp_aeval_apply, Algebra.Presentation.relation_comp_localizationAway_inl, WittVector.coeff_select, aeval_unique, coeff_rTensorAlgHom_monomial_tmul, bind₁_bind₁, algebraTensorAlgEquiv_symm_map, rename_polynomial_aeval_X, coeff_expand_of_not_dvd, Algebra.Generators.Hom.equivAlgHom_symm_apply_val, tensorEquivSum_C_tmul_one, map_iterateFrobenius_expand, Polynomial.toMvPolynomial_X, sumAlgEquiv_apply, Algebra.Generators.ker_comp_eq_sup, Algebra.Generators.ofComp_toAlgHom_monomial_sumElim, exists_finset_rename₂, algebraMap_eq, algebraicIndependent_X, eval_toMvPolynomial, Algebra.Presentation.algebraTensorAlgEquiv_symm_relation, Algebra.Generators.aeval_val_eq_zero, coeffsIn_pow, esymmAlgHom_apply, aeval_eq_eval₂Hom, rename_prod_mk_eval₂, AlgebraicIndependent.aevalEquivField_apply_coe, IsSymmetric.smul, aeval_C, IsTranscendenceBasis.mvPolynomial, toMvPowerSeries_pUnitAlgEquiv, transcendental_polynomial_aeval_X, pderiv_map, aeval_comp_expand, Algebra.Generators.naive_σ, AlgebraicIndependent.aevalEquiv_apply_coe, rename_C, StandardEtalePresentation.aeval_val_equivMvPolynomial, aevalTower_comp_toAlgHom, restrictSupport_add, IsHomogeneous.rename_isHomogeneous, WittVector.polyOfInterest_vars_eq, pderiv_inr_universalFactorizationMap_X, sumAlgEquiv_symm_apply, eval₂_pUnitAlgEquiv_symm, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, Algebra.Generators.ker_eq_ker_aeval_val, instIsPushout_1, supported_empty, Algebra.Generators.toExtension_algebra₁, KaehlerDifferential.mvPolynomialBasis_repr_D, pderiv_eq_zero_of_notMem_vars, aeval_C_comp_left, transcendental_X, degrees_rename_of_injective, PolynomialLaw.range_φ, mapAlgHom_apply, Algebra.Generators.cotangentRestrict_mk, optionEquivLeft_monomial, Algebra.SubmersivePresentation.ofSubsingleton_algebra_smul, KaehlerDifferential.mvPolynomialBasis_repr_comp_D, WittVector.bind₁_onePoly_wittPolynomial, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, optionEquivLeft_symm_apply, algebraTensorAlgEquiv_tmul, mem_support_coeff_finSuccEquiv, Algebra.Generators.aeval_val_σ', Algebra.Generators.Hom.toAlgHom_id, Algebra.Generators.Hom.comp_val, instIsPushout, comap_apply, vars_rename, WittVector.bind₁_zero_wittPolynomial, IsTranscendenceBasis.mvPolynomial', StandardEtalePresentation.toPresentation_val, rename_comp_bind₁, aeval_id_eq_join₁, rename_X, pUnitAlgEquiv_monomial, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, Algebra.mvPolynomial, comap_id_apply, aeval_one_tmul, smul_eq_C_mul, finSuccEquiv_rename_finSuccEquiv, rename_expand, homogeneousSubmodule_one_pow, universalFactorizationMapPresentation_algebra_smul, MonomialOrder.degree_smul, Algebra.FiniteType.instMvPolynomialOfFinite, IsHomogeneous.sum_X_mul_pderiv, derivation_C_mul, aeval_sumElim_pderiv_inl, AnalyticAt.aeval_mvPolynomial, tensorEquivSum_one_tmul_X, supported_univ, isSymmetric_rename, universalFactorizationMap_freeMonic, Algebra.Generators.Hom.toAlgHom_monomial, universalFactorizationMapPresentation_val, rename_comp_rename, coe_expand, aeval_sumElim, universalFactorizationMapPresentation_σ', aeval_comp_rename, KaehlerDifferential.mvPolynomialBasis_repr_symm_single, mem_symmetricSubalgebra, eval₂_rename_prod_mk, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, mapAlgHom_coe_ringHom, bind₁_wittPolynomial_xInTermsOfW, Algebra.FinitePresentation.out, rename_leftInverse, Algebra.FiniteType.iff_quotient_mvPolynomial'', esymmAlgHom_fin_bijective, esymmAlgEquiv_apply, mem_vanishingIdeal_iff, mem_vanishingIdeal_singleton_iff, expand_zmod, aeval_zero', weightedTotalDegree_rename_of_injective, range_mapAlgHom, rename_toMvPolynomial, aeval_rename, WittVector.bind₁_frobeniusPolyRat_wittPolynomial, optionEquivLeft_symm_C_X, WittVector.aeval_verschiebungPoly, eval₂Hom_bind₁, finSuccEquiv_X_zero, degreeOf_eq_natDegree, bind₁_X_right, coeff_rename_eq_zero, eval₂Hom_C_left, transcendental_supported_polynomial_aeval_X_iff, aeval_monomial, StandardEtalePresentation.toPresentation_relation, Polynomial.toMvPolynomial_injective, Algebra.PreSubmersivePresentation.ofHasCoeffs_val, Algebra.Generators.self_algebra_algebraMap, pderiv_X_self, WittVector.mul_polyOfInterest_aux3, pderiv_C, universalFactorizationMapPresentation_jacobiMatrix, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul, MvRatFunc.rank_eq_max_lift, aeval_prod, homogeneousSubmodule_mul, Matrix.toMvPolynomial_mul, Polynomial.Bivariate.pderiv_one_equivMvPolynomial, exists_restrict_to_vars, wittStructureInt_rename, algebraTensorAlgEquiv_symm_monomial, aevalTower_algebraMap, optionEquivLeft_elim_eval, optionEquivLeft_symm_X, SymmetricAlgebra.IsSymmetricAlgebra.mvPolynomial, renameEquiv_symm, eval_expand, aeval_comp_toMvPolynomial, supportedEquivMvPolynomial_symm_C, tensorEquivSum_X_tmul_one, expand_mul_eq_comp, eval₂_pUnitAlgEquiv, supported_eq_range_rename, trdeg_of_isDomain, rename_hsymm, MonomialOrder.sPolynomial_decomposition', transcendental_supported_X, aeval_natDegree_le, optionEquivLeft_symm_C_C, C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum, Algebra.Generators.Hom.algebraMap_toAlgHom, WittVector.coeff_frobenius, Algebra.Generators.comp_σ, tensorEquivSum_C_tmul_C, IsHomogeneous.finSuccEquiv_coeff_isHomogeneous, Algebra.Presentation.instFinitePresentationQuotientOfFinite, MvPowerSeries.subst_coe, mapEquivMonic_symm_map_algebraMap, coe_aeval_eq_eval, exists_integral_inj_algHom_of_fg, Polynomial.Bivariate.equivMvPolynomial_C_C, Algebra.Generators.ker_naive, instFreeMvPolynomialKaehlerDifferential, hom_bind₁, coeff_expand_zero, Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, Matrix.mvPolynomialX_mapMatrix_aeval, supported_eq_vars_subset, Polynomial.aeval_homogenize_of_eq_one, rename_eq, totalDegree_coeff_optionEquivLeft_le, derivation_ext_iff, mapEquivMonic_symm_map, IsHomogeneous.pderiv, Algebra.SubmersivePresentation.basisDeriv_apply, bind₁_monomial, MonomialOrder.degree_smul_of_mem_nonZeroDivisors, Algebra.Presentation.mem_ker_naive, C_eq_smul_one, esymmAlgHom_surjective, aevalTower_ofNat, esymmAlgEquiv_symm_apply, instIsPushoutFractionRingMvPolynomial_1, rename_surjective, eval₂Hom_comp_expand, Polynomial.toMvPolynomial_C, Algebra.Generators.Hom.equivAlgHom_apply_coe, universalFactorizationMapPresentation_jacobian, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap, esymmAlgHom_injective, commAlgEquiv_C_X, expand_zero_apply, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap', renameSymmetricSubalgebra_apply_coe, Algebra.FinitePresentation.iff_quotient_mvPolynomial', coe_mapEquivMonic_comp, transcendental_supported_polynomial_aeval_X, instIsPushoutFractionRingMvPolynomial, eval_polynomial_eval_finSuccEquiv, constantCoeff_comp_algebraMap, pderiv_inl_universalFactorizationMap_X, rename_id, Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val, rTensorAlgHom_apply_eq
coeff 📖	CompOp	103 math math: 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, coeff_expand_smul, MonomialOrder.coeff_eq_zero_of_lt, coeff_C, coeff_X, 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, eval_eq', ext_iff, 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, totalDegree_eq_zero_iff_eq_C, coeff_sumSMulX, coeff_rename_mapDomain, 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, MvPowerSeries.coeff_truncFun', homogeneousComponent_apply, coeff_mul_X', coeff_mul_X, coeff_rTensorAlgHom_tmul, optionEquivLeft_coeff_some_coeff_none, mem_coeffsIn, coeff_mem_coeffs, C_dvd_iff_dvd_coeff, homogeneousComponent_zero, coeff_map, FirstOrder.Ring.MvPolynomialSupportLEEquiv_symm_apply_coeff, coeff_zero, coeff_modMonomial_of_not_le, coeff_X', MvPowerSeries.coeff_truncFun, 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, 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_weightedHomogeneousComponent, MonomialOrder.coeff_mul_of_degree_add, MonomialOrder.coeff_sPolynomial_sup_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_eq_zero_of_totalDegree_lt, coeff_expand_zero, weightedHomogeneousComponent_apply, coeff_mul, mem_image_comap_C_basicOpen, coeff_sum
coeffAddMonoidHom 📖	CompOp	1 math math: coeffAddMonoidHom_apply
coeffs 📖	CompOp	19 math math: 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 math math: 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
commSemiring 📖	CompOp	1435 math math: pUnitAlgEquiv_symm_monomial, funext_iff, eval_indicator_apply_eq_one, join₁_rename, vanishingIdeal_anti_mono, aeval_sum, dvd_monomial_one_iff_exists, WittVector.bind₁_frobeniusPoly_wittPolynomial, KaehlerDifferential.mvPolynomialBasis_apply, MvPowerSeries.WithPiTopology.tendsto_trunc_atTop, support_sum, MonomialOrder.sPolynomial_leadingTerm_mul', coe_C, Algebra.PreSubmersivePresentation.jacobiMatrix_naive, support_mul, algHom_ext_iff, MonomialOrder.span_leadingTerm_sdiff_singleton_zero, map_bind₁, vars_sum_of_disjoint, totalDegree_monomial, Algebra.Generators.aeval_val_surjective, mul_X_divMonomial, radical_le_vanishingIdeal_zeroLocus, wittPolynomial_zmod_self, aeval_X_left, map_mapRange_eq_iff, map_comp_C, DirectSum.coeLinearMap_eq_dfinsuppSum, coeffs_add, MvPowerSeries.eq_iff_frequently_trunc'_eq, pUnitAlgEquiv_apply, eval₂Hom_X, toMvPowerSeries_uniformContinuous, exists_finset_rename, MonomialOrder.monic_X_sub_C, hom_C, weightedHomogeneousComponent_of_isWeightedHomogeneous_same, Polynomial.homogenize_map, MvPowerSeries.trunc'_trunc', support_finSuccEquiv, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, rTensor_apply_tmul_apply, degrees_monomial, zero_divMonomial, Ideal.mem_span_iff_exists_isHomogeneous, WittVector.aeval_verschiebung_poly', MonomialOrder.degree_add_of_ne, rTensorAlgEquiv_apply, one_def, Algebra.Generators.H1Cotangent.δAux_mul, Algebra.Presentation.naive_toGenerators, mem_image_support_coeff_finSuccEquiv, mapEquiv_symm, scalarRTensor_apply_monomial_tmul, comapEquiv_symm_coe, homogeneousComponent_eq_zero', WeierstrassCurve.Projective.eval_polynomial, Matrix.charpoly.univ_map_map, eval₂_expand, isOpenMap_comap_C, universalFactorizationMap_comp_map, aeval_algebraMap_eq_zero_iff, isScalarTower_right, MonomialOrder.degree_monomial, coeff_X_mul', Algebra.PreSubmersivePresentation.ofHasCoeffs_map, expand_X, algebraicIndependent_iff_ker_eq_bot, IsSymmetric.map, Algebra.Generators.cotangentSpaceBasis_apply, IsWeightedHomogeneous.pderiv, instIsReduced, X_pow_eq_monomial, isEmptyRingEquiv_apply, WittVector.ghostComponent_apply, ker_map, map_leftInverse, aeval_wittPolynomial, KaehlerDifferential.mvPolynomialBasis_repr_D_X, optionEquivLeft_C, rename_rename, iterToSum_sumToIter, Algebra.Generators.toAlgHom_ofComp_localizationAway, Polynomial.homogenize_smul, divMonomial_add_modMonomial, MvPowerSeries.trunc'_expand_trunc', optionEquivLeft_X_some, MonomialOrder.leadingCoeff_eq_zero_iff, eval₂Hom_monomial, aeval_X_left_apply, Polynomial.toPowerSeries_toMvPowerSeries, le_vanishingIdeal_zeroLocus, homogeneousComponent_mem, pUnitAlgEquiv_symm_apply, expand_eq_zero, WeierstrassCurve.Jacobian.baseChange_polynomialZ, support_monomial, Algebra.Presentation.localizationAway_relation, monomial_finsupp_sum_index, weightedHomogeneousSubmodule_mul, Ideal.span_pow_eq_map_homogeneousSubmodule, coeffs_mul_X, mul_def, natDegree_finSuccEquiv, StandardEtalePresentation.toPresentation_algebra_smul, totalDegree_X_pow, Ideal.span_eq_map_homogeneousSubmodule, bind₂_comp_C, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C, eval₂_zero'_apply, image_comap_C_basicOpen, degreeOf_C, WeierstrassCurve.Projective.polynomial_relation, Matrix.toMvPolynomial_add, algHom_ext'_iff, IntermediateField.mem_adjoin_iff, AlgebraicIndependent.repr_ker, MonomialOrder.leadingCoeff_mul_of_isRegular_right, mem_range_map_iff_coeffs_subset, aeval_X, comapEquiv_coe, exists_dvd_map_of_isAlgebraic, Polynomial.pUnitAlgEquiv_symm_toPowerSeries, scalarRTensor_apply_X_tmul_apply, MvPowerSeries.ext_trunc', smul_monomial, eval₂_pow, AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin, MonomialOrder.leadingCoeff_mul, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, AnalyticOnNhd.eval_linearMap', IsWeightedHomogeneous.weightedHomogeneousComponent_same, optionEquivLeft_apply, instIsScalarTower, bind₂_C_left, totalDegree_coeff_finSuccEquiv_add_le, map_comp_rename, ACounit_X, WittVector.mul_polyOfInterest_aux2, prime_rename_iff, bind₁_xInTermsOfW_wittPolynomial, WeierstrassCurve.Jacobian.eval_polynomialY, constantCoeff_rename, eval₂_prod, Algebra.PreSubmersivePresentation.jacobiMatrix_reindex, map_bind₂, iterToSum_C_X, AlgebraicClosure.maxIdeal.isMaximal, map_eval₂, eval_map, CommRingCat.free_map_coe, Algebra.FinitePresentation.mvPolynomial_of_finitePresentation, Algebra.SubmersivePresentation.ofSubsingleton_algebra_algebraMap, killCompl_comp_rename, map_eval₂Hom, supportedEquivMvPolynomial_symm_X, pderiv_one, mkDerivation_X, pderiv_mul, Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp, char_dvd_card_solutions_of_add_lt, comp_eval₂Hom, ACounit_surjective, supported_eq_adjoin_X, eval₂_zero, degreeOf_mul_le, degreeOf_sum_le, aeval_eq_eval, schwartz_zippel_totalDegree, aeval_ite_mem_eq_self, support_sdiff_support_subset_support_add, Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs, IsWeightedHomogeneous.mul, eval₂Hom_C_id_eq_join₁, eval_mem, PolynomialLaw.exists_lift', Algebra.Generators.algebraMap_surjective, totalDegree_add_eq_right_of_totalDegree_lt, pow_idealOfVars, join₂_comp_map, comap_id, eval_rename_prod_mk, optionEquivRight_C, monomial_zero, map_mvPolynomial_eq_eval₂, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_one_equivMvPolynomial, eval_eval₂, aevalTower_comp_C, rename_msymm, comap_comp_apply, eval₂_id, eval₂Hom_C_eq_bind₁, sum_antidiagonal_card_esymm_psum_eq_zero, X_mul_cancel_right_iff, Algebra.PreSubmersivePresentation.ofHasCoeffs_relation, degreeOf_coeff_finSuccEquiv, mem_pow_idealOfVars_iff, X_prime, rename_id_apply, constantCoeff_C, MvPowerSeries.trunc_C, map_map, support_eq_empty, eval₂Hom_comp_bind₂, coe_one, nonempty_support_finSuccEquiv, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, pderiv_rename, Algebra.Presentation.comp_relation_inr, monomial_eq_monomial_iff, LinearMap.nilRankAux_basis_indep, MonomialOrder.leadingTerm_zero, eval₂_mul_monomial, weightedHomogeneousComponent_zero, AlgebraicIndependent.aeval_comp_repr, esymmAlgHomMonomial_single, homogeneousComponent_C_mul, IsHomogeneous.map, map_expand, MonomialOrder.image_leadingTerm_sdiff_singleton_zero, map_aeval, instFree, map_frobenius_expand, coeffs_one, renameEquiv_trans, weightedDecomposition.decompose'_apply, FirstOrder.Ring.lift_genericPolyMap, faithfulSMul, coeffs_one_of_nontrivial, expand_monomial, expand_char, monomial_mul_mem_coeffsIn, eval₂Hom_congr, WeierstrassCurve.Jacobian.eval_polynomialX_of_Z_ne_zero, map_rename, Algebra.PreSubmersivePresentation.ofHasCoeffs_σ', killCompl_C, Algebra.Presentation.quotientEquiv_symm, eval₂_const_pUnitAlgEquiv_symm, eval_comp_toMvPolynomial, Algebra.Generators.H1Cotangent.δAux_C, Algebra.Generators.map_toComp_ker, support_finSuccEquiv_nonempty, Algebra.Generators.Hom.toExtensionHom_toAlgHom_apply, eval₂_sum, bind₁_X_left, monomial_one_dvd_iff_modMonomial_eq_zero, sumAlgEquiv_comp_rename_inr, aevalTower_toAlgHom, Algebra.Generators.ofComp_val, coe_eq_one_iff, Algebra.Presentation.map_relationOfHasCoeffs, LinearMap.polyCharpoly_coeff_isHomogeneous, eval₂_map, X_mul_pderiv_monomial, MonomialOrder.degree_add_le, degree_optionEquivLeft, mapAlgHom_id, Algebra.Generators.naive_val, MonomialOrder.leadingCoeff_prod_of_regular, totalDegree_list_prod, coeff_expand_smul, Algebra.Generators.algebraMap_apply, map_esymm, weightedHomogeneousComponent_eq_zero', IsHomogeneous.add, coe_eq_zero_iff, expand_C, MvPowerSeries.trunc'_trunc'_pow, MonomialOrder.eq_C_of_degree_eq_zero, coeffs_C, smulCommClass, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, optionEquivRight_X_none, homogeneousComponent_isHomogeneous, rename_psum, Algebra.Generators.map_ofComp_ker, WeierstrassCurve.Jacobian.polynomialY_eq, sum_homogeneousComponent, expand_zero, support_add, degreesLE_nsmul, coe_monomial, WeierstrassCurve.Jacobian.eval_polynomialX, totalDegree_rename_le, C_apply, MonomialOrder.leadingCoeff_mul_of_right_mem_nonZeroDivisors, coe_mapEquivMonic_comp', Algebra.Presentation.naive_relation, WeierstrassCurve.Projective.eval_polynomialX, WeierstrassCurve.Projective.baseChange_polynomial, Matrix.toMvPolynomial_map, single_eq_monomial, Polynomial.toMvPolynomial_eq_rename_comp, MvPowerSeries.trunc_one, Polynomial.aeval_homogenize_X_one, adjoin_range_X, mul_X_mem_coeffsIn, coeff_C, WeierstrassCurve.Jacobian.eval_polynomialY_of_Z_ne_zero, MonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure, AddMonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure, bind₂_map, totalDegree_mul_of_isDomain, X_dvd_X, transcendental_polynomial_aeval_X_iff, aeval_algebraMap_eq_zero_iff_of_injective, Algebra.Generators.algebraMap_eq, Algebra.SubmersivePresentation.ofSubsingleton_relation, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, MonomialOrder.leadingTerm_monomial, X_mul_mem_coeffsIn, support_rename_of_injective, Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial, comap_comp, eval_ofNat, MonomialOrder.degree_mul_leadingTerm, xInTermsOfW_eq, LinearMap.nilRank_eq_polyCharpoly_natTrailingDegree, eval_eq_eval_mv_eval', degrees_map_of_injective, ACounit_C, LinearMap.polyCharpoly_baseChange, transcendental_supported_X_iff, Polynomial.homogenize_add, vanishingIdeal_pointToPoint, optionEquivLeft_X_none, algebraicIndependent_polynomial_aeval_X, IsHomogeneous.HomogeneousSubmodule.gcommSemiring, degreeOf_rename_of_injective, degreesLE_add, exists_rename_eq_of_vars_subset_range, MonomialOrder.span_leadingTerm_eq_span_monomial, optionEquivRight_symm_apply, instIsPrimeVanishingIdealSingletonForallSet, eval₂Hom_zero_apply, scalarRTensor_apply_tmul, degrees_C, WeierstrassCurve.Jacobian.polynomial_relation, LinearMap.polyCharpolyAux_map_eval, eval_prod, C_mul_X_eq_monomial, Algebra.Generators.Hom.aeval_val, Polynomial.MonicDegreeEq.freeMonic_coe, degreeOf_mul_eq, Algebra.Presentation.comp_aeval_relation_inl, C_0, WittVector.mulN_coeff, bind₂_monomial, isUnit_iff_totalDegree_of_isReduced, totalDegree_finset_prod, monomialOneHom_apply, pderiv_sumToIter, coeff_homogeneousComponent, support_expand_subset, MonomialOrder.coeff_prod_sum_degree, totalDegree_C, WeierstrassCurve.Projective.polynomialZ_eq, IsSymmetric.one, Matrix.charpoly.univ_monic, totalDegree_pow, coeff_rename_embDomain, isUnit_iff, monomial_left_inj, X_dvd_monomial, coe_zero, finSuccEquiv_coeff_coeff, rename_comp_expand, Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, Algebra.PreSubmersivePresentation.jacobiMatrix_apply, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C', coeff_C_mul, rename_esymm, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply, quotient_map_C_eq_zero, iterToSum_X, coeff_X_pow, C_mul_monomial, Algebra.Generators.H1Cotangent.δAux_monomial, vars_monomial, pow_idealOfVars_eq_span, AnalyticOnNhd.eval_linearMap, IsHomogeneous.pow, IsWeightedHomogeneous.sum, Algebra.Generators.toAlgHom_ofComp_surjective, bind₁_comp_bind₁, commAlgEquiv_C, coeff_zero_C, Algebra.Generators.Hom.algebraMap_toAlgHom', Algebra.Generators.cotangentSpaceBasis_repr_tmul, MonomialOrder.monic_X_add_C, aevalTower_X, bind₂_monomial_one, commAlgEquiv_X, mapEquiv_apply, eval₂Hom_congr', Matrix.charpoly.univ_coeff_eval₂Hom, optionEquivRight_X_some, aeval_expand, AlgebraicIndependent.lift_reprField, instCharZero, aeval_algebraMap_apply, C_1, eval₂Hom_X', eval₂_one, rTensor_apply_X_tmul, Algebra.SubmersivePresentation.map_invJacobianOfHasCoeffs, Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation, wittPolynomial_one, pderiv_X, eval_eq', uniqueFactorizationMonoid, restrictSupport_univ, Algebra.Generators.H1Cotangent.δAux_toAlgHom, eval₂_C, Subalgebra.mvPolynomial_aeval_coe, IsLocalization.Away.mvPolynomialQuotientEquiv_apply, Algebra.Presentation.naive_relation_apply, C_add, PolynomialLaw.exists_lift, isHomogeneous_C_mul_X, WittVector.mul_polyOfInterest_aux4, rename_eval₂, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some, coeff_smul, MvPowerSeries.expand_eq_expand, irreducible_of_disjoint_support, Algebra.Generators.localizationAway_σ, isWeightedHomogeneous_one, mapAlgEquiv_apply, Polynomial.Bivariate.equivMvPolynomial_symm_X_0, algebraTensorAlgEquiv_symm_comp_aeval, finitePresentation_universalFactorizationMap, mapAlgEquiv_refl, WittVector.frobeniusPoly_zmod, totalDegree_multiset_prod, eval_neg, Algebra.FiniteType.iff_quotient_mvPolynomial', map_restrict_dom_evalₗ, tensorEquivSum_one_tmul_C, rTensor_apply_tmul, IsWeightedHomogeneous.weightedHomogeneousComponent_ne, IsSymmetric.mul, WeierstrassCurve.Jacobian.baseChange_polynomialY, MonomialOrder.Monic.pow, MonomialOrder.degree_mul_of_isRegular_right, map_ofNat, Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom, coeff_monomial_mul, Polynomial.degree_freeMonic, IsWeightedHomogeneous.add, eval₂Hom_rename, degreeOf_pow_eq, LieModule.rank_eq_natTrailingDegree, bind₂_id, X_mul_cancel_left_iff, sumAlgEquiv_comp_rename_inl, dvd_monomial_iff_exists, WeierstrassCurve.Projective.baseChange_polynomialY, AlgebraicIndependent.aeval_of_algebraicIndependent, aeval_bind₁, MonomialOrder.degree_sum_le, MonomialOrder.degree_mul_of_mul_leadingCoeff_ne_zero, MonomialOrder.leadingCoeff_pow_of_pow_leadingCoeff_ne_zero, DirectSum.coeAddMonoidHom_eq_support_sum, algebraMap_apply, mkDerivationₗ_monomial, exists_fin_rename, LinearMap.toMvPolynomial_baseChange, optionEquivLeft_coeff_coeff, IsWeightedHomogeneous.sum_weight_X_mul_pderiv, Matrix.charpoly.optionEquivLeft_symm_univ_isHomogeneous, sum_weightedHomogeneousComponent, C_surjective, pderiv_def, isEmptyRingEquiv_symm_apply, MonomialOrder.degree_leadingTerm_mul, mem_pow_idealOfVars_iff', mem_supported, Matrix.toMvPolynomial_zero, renameEquiv_apply, degrees_pow_le, rename_esymmAlgHom, aeval_eq_zero, eval₂_cast_comp, Algebra.PreSubmersivePresentation.naive_toPresentation, Polynomial.eval_homogenize, modMonomial_add_divMonomial, MonomialOrder.span_leadingTerm_eq_span_monomial', bind₁_C_right, coe_coeffs_map, decompose'_apply, instIsLocalHomRingHomAlgebraMap, WittVector.bind₁_wittMulN_wittPolynomial, PolynomialLaw.exists_range_φ_eq_of_fg, Algebra.FinitePresentation.mvPolynomial, coeff_single_X_pow, MonomialOrder.degree_X_sub_C, monomial_one_mul_cancel_left_iff, eq_zero_iff, aevalTower_C, expand_one_apply, coe_basisMonomials, map_expand_pow_char, xInTermsOfW_aux, Algebra.Presentation.span_range_relation_eq_ker, MonomialOrder.degree_mul_lt_iff_left_lt_of_ne_zero, mapRange_eq_map, monomial_mem_pow_idealOfVars_iff, MonomialOrder.degree_smul_le, irreducible_sumSMulX, AnalyticOnNhd.aeval_mvPolynomial, totalDegree_eq_zero_iff_eq_C, Algebra.Generators.Hom.toAlgHom_X, bind₁_rename, smulCommClass_right, degreeOf_mul_X_eq_degreeOf_add_one_iff, wittStructureRat_prop, WeierstrassCurve.Projective.eval_polynomialX_of_Z_ne_zero, degrees_rename, Algebra.Presentation.comp_relation, eval₂Hom_zero', Polynomial.Bivariate.equivMvPolynomial_symm_C, Algebra.Generators.instIsScalarTowerRing, MvPowerSeries.aeval_coe, Polynomial.homogenize_X_pow, WittVector.IsPoly.poly, map_hsymm, finite_universalFactorizationMap, rTensorAlgHom_toLinearMap, wittStructureRat_rec, WittVector.mul_polyOfInterest_vars, isRegular_prod_X, homogeneousSubmodule_zero, expand_eq_C, MvPowerSeries.trunc'_expand, universalFactorizationMapPresentation_map, coeff_rename_mapDomain, MonomialOrder.degree_mul_le, restrictSupport_mono, algebraTensorAlgEquiv_symm_X, expand_injective, mem_restrictDegree, support_coeff_finSuccEquiv, MonomialOrder.monic_monomial, Algebra.Presentation.aeval_val_relation, LinearMap.polyCharpolyAux_map_eq_charpoly, expand_one, degrees_map_le, esymmAlgHom_fin_surjective, expand_inj, LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff, indicator_mem_restrictDegree, coeffsIn_mul, eval_eq, MonomialOrder.sPolynomial_def, Algebra.Generators.H1Cotangent.δAux_ofComp, restrictSupport_zero, as_sum, MonomialOrder.degree_mul_of_left_mem_nonZeroDivisors, isUnit_iff_eq_C_of_isReduced, MonomialOrder.leadingCoeff_monomial, psum_zero, monomial_add_single, le_coeffsIn_pow, supported_strictMono, IsWeightedHomogeneous.pow, MonomialOrder.degree_pow_le, eval_add, WeierstrassCurve.Projective.map_polynomialX, pointToPoint_zeroLocus_le, Algebra.SubmersivePresentation.map_jacobianRelationsOfHasCoeffs, exists_integral_inj_algHom_of_quotient, MvPowerSeries.trunc_map, isNilpotent_iff, instNoZeroDivisors, exists_finite_inj_algHom_of_fg, MonomialOrder.monic_monomial_one, zeroLocus_bot, WeierstrassCurve.Jacobian.baseChange_polynomial, aeval_def, monomial_eq_zero, eval_monomial, MonomialOrder.degree_C, coeff_monomial_mul', monomial_mem_coeffsIn, coe_eval₂Hom, MvPowerSeries.coeff_trunc', vars_C_mul, Algebra.Generators.toAlgHom_ofComp_rename, Algebra.FinitePresentation.iff, wittStructureRat_rec_aux, Polynomial.Bivariate.equivMvPolynomial_symm_X_1, eval₂_add, MonomialOrder.image_leadingTerm_insert_zero, WeierstrassCurve.Projective.eval_polynomialZ, supported_mono, Algebra.Generators.ker_localizationAway, MonomialOrder.sPolynomial_decomposition, constantCoeff_smul, totalDegree_expand, algHom_C, leadingCoeff_toLex_C, support_mul_X, wittStructureInt_prop, eval_pow, eval₂Hom_zero'_apply, psumPart_zero, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, le_zeroLocus_iff_le_vanishingIdeal, MonomialOrder.leadingCoeff_mul_of_left_mem_nonZeroDivisors, derivation_C, mem_support_coeff_optionEquivLeft, Algebra.Presentation.fg_ker, dvd_smul_X_iff_exists, Algebra.Generators.σ_smul, MvPowerSeries.coeff_trunc, mem_supported_vars, mkDerivation_monomial, degrees_sum_le, Algebra.Presentation.relation_mem_ker, Algebra.Generators.Hom.toExtensionHom_toRingHom, schwartz_zippel_sup_sum, mem_map_C_iff, rename_monomial, aeval_toMvPolynomial, mul_esymm_eq_sum, prime_C_iff, eval_mul, restrictScalars_restrictSupportIdeal, instFiniteSubtypeMemSubmoduleRestrictDegreeOfFinite, mem_restrictSupport_iff, degreesLE_zero, universalFactorizationMapPresentation_relation, aevalTower_comp_algebraMap, eval₂_zero_apply, Algebra.PreSubmersivePresentation.aevalDifferential_single, isWeightedHomogeneous_monomial, AlgebraicIndependent.algebraMap_aevalEquiv, isWeightedHomogeneous_zero, MonomialOrder.coeff_degree_eq_zero_iff, aeval_id_rename, degreeOf_mul_X_self, eq_C_of_isEmpty, coeff_one, WeierstrassCurve.Projective.polynomialX_eq, Algebra.adjoin_range_eq_range_aeval, monomial_zero', Polynomial.homogenize_finsetSum, weightedHomogeneousComponent_directSum, Algebra.Generators.aeval_val_σ, msymm_zero, totalDegree_add, Polynomial.homogenize_C_mul, mem_zeroLocus_iff, coe_add, totalDegree_coeff_optionEquivLeft_add_le, modMonomial_X, homogeneousComponent_apply, vars_prod, MonomialOrder.leadingCoeff_add_of_lt, eval_indicator_apply_eq_zero, sumToIter_iterToSum, divMonomial_mul_monomial, map_surjective_iff, constantCoeff_wittPolynomial, WeierstrassCurve.Projective.polynomialY_eq, aeval_eq_constantCoeff_of_vars, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul, weightedHomogeneousComponent_finsupp, WeierstrassCurve.Projective.negDblY_eq, SymmetricAlgebra.equivMvPolynomial_symm_X, expand_bind₁, map_injective_iff, linearIndependent_X, coeff_mul_X', prod_X_pow_eq_monomial, map_injective, constantCoeff_monomial, coeff_mul_X, smul_eval, eval₂Hom_zero, MvPowerSeries.substAlgHom_coe, universalFactorizationMapPresentation_algebra_algebraMap, degrees_one, C_eq_zero, supDegree_toLex_C, WeierstrassCurve.Projective.eval_polynomialY_of_Z_ne_zero, coeff_rTensorAlgHom_tmul, aeval_zero, killCompl_rename_app, mem_weightedHomogeneousSubmodule, comp_aeval, support_map_of_injective, constantCoeff_X, divMonomial_monomial, frobenius_zmod, KaehlerDifferential.mvPolynomialBasis_repr_apply, WittVector.frobeniusPolyAux_eq, optionEquivLeft_coeff_some_coeff_none, IntermediateField.mem_adjoin_range_iff, WittVector.coeff_frobeniusFun, renameEquiv_refl, totalDegree_renameEquiv, expand_mul, mem_coeffsIn, Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul, WeierstrassCurve.Projective.baseChange_polynomialX, isLocalHom_expand, Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, weightedHomogeneousComponent_of_isWeightedHomogeneous_ne, C_mul', AlgebraicClosure.le_maxIdeal, isEmptyAlgEquiv_apply, bind₂_X_right, Algebra.Generators.cMulXSubOneCotangent_eq, map_C, isHomogeneous_monomial, LinearMap.polyCharpolyAux_baseChange, Polynomial.Bivariate.equivMvPolynomial_X, C_dvd_iff_dvd_coeff, pderiv_C_mul, Polynomial.homogenize_finsetProd, Module.Basis.symmetricAlgebra_repr_apply, MonomialOrder.degree_smul_of_isRegular, AlgebraicClosure.toSplittingField_coeff, eval₂_mul, Matrix.toMvPolynomial_eval_eq_apply, coe_pow, MonomialOrder.degree_one, natDegree_optionEquivLeft, Matrix.charpoly.univ_coeff_isHomogeneous, isHomogeneous_one, ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial, WittVector.constantCoeff_wittMul, Algebra.Generators.self_algebra_smul, decomposition.decompose'_apply, restrictSupport_nsmul, mem_support_finSuccEquiv, psum_one, mem_degreesLE, weightedHomogeneousComponent_isWeightedHomogeneous, isNoetherianRing_fin, X_dvd_iff_modMonomial_eq_zero, funext_set_iff, X_mul_divMonomial, map_monomial, monomial_mem_restrictSupport, algebraicIndependent_iff_injective_aeval, vars_map_of_injective, aeval_map_algebraMap, Algebra.Generators.Hom.toAlgHom_C, rename_comp_toMvPolynomial, comap_C_surjective, finSuccEquiv_comp_C_eq_C, esymmAlgHom_zero, homogeneousComponent_eq_zero, eval₂_eta, coeToMvPowerSeries.algHom_apply, AlgebraicIndependent.liftAlgHom_comp_reprField, rename_rightInverse, char_dvd_card_solutions, WeierstrassCurve.Jacobian.polynomialZ_eq, MonomialOrder.sPolynomial_monomial_mul, hsymmPart_zero, eval₂Hom_map_hom, isRegular_X, mem_homogeneousSubmodule, finSuccEquiv_eq, char_dvd_card_solutions_of_sum_lt, SymmetricAlgebra.equivMvPolynomial_ι_apply, RingHom.IsStandardSmooth.exists_etale_mvPolynomial, homogeneousComponent_zero, LinearMap.polyCharpoly_eq_of_basis, ker_eval₂Hom_universalFactorizationMap, monomial_left_injective, bind₁_comp_rename, coeff_map, monomial_sum_index, degrees_prod_le, LinearMap.polyCharpolyAux_map_aeval, Matrix.mvPolynomialX_mapMatrix_eval, monic_monomial_eq, image_support_finSuccEquiv, pderiv_monomial_single, degreeOf_prod_eq, eval₂_rename, AlgebraicIndependent.aeval_repr, support_expand, MonomialOrder.degree_eq_zero_iff, add_divMonomial, instFiniteSubtypeMemSubmoduleRestrictTotalDegreeOfFinite, Polynomial.Bivariate.equivMvPolynomial_C_X, IsSymmetric.rename, IsHomogeneous.aeval, isEmptyRingEquiv_symm_toRingHom, MonomialOrder.leadingTerm_C, DirectSum.coeLinearMap_eq_finsum, WittVector.mul_polyOfInterest_aux1, support_monomial_subset, monomial_mul, quotientEquivQuotientMvPolynomial_leftInverse, MvPowerSeries.totalDegree_trunc', aeval_bind₂, rename_bind₁, support_X_pow, rTensor_symm_apply_single, pderiv_X_of_ne, prod_X_add_C_coeff, renameSymmetricSubalgebra_symm_apply_coe, IsSymmetric.zero, Algebra.Generators.Hom.toAlgHom_comp_apply, degree_finSuccEquiv, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, isNoetherianRing_fin_0, nonempty_support_optionEquivLeft, pderiv_monomial, isRegular_X_pow, Algebra.adjoin_eq_range, degrees_add_le, mapAlgEquiv_symm, Algebra.Generators.toComp_toAlgHom_monomial, counit_surjective, rename_injective, isHomogeneous_zero, degrees_mul_le, WeierstrassCurve.Projective.negDblY_eq', monomial_mem_homogeneousSubmodule_pow_degree, Algebra.SubmersivePresentation.aeval_jacobianOfHasCoeffs, LinearMap.polyCharpolyAux_coeff_eval, esymmAlgHomMonomial_single_one, AlgebraicClosure.Monics.map_eq_prod, coe_smul, MonomialOrder.degree_prod_le, totalDegree_add_eq_left_of_totalDegree_lt, map_rightInverse, dvd_monomial_mul_iff_exists, killCompl_map, MonomialOrder.span_leadingTerm_insert_zero, Algebra.FiniteType.iff_quotient_mvPolynomial, MonomialOrder.div_set, aeval_eq_bind₁, support_optionEquivLeft, X_mul_modMonomial, degreeOf_pow_le, dvd_X_iff_exists, finSuccEquiv_X_succ, aeval_ofNat, MonomialOrder.degree_zero, Algebra.Presentation.aeval_val_relationOfHasCoeffs, eval₂Hom_eq_zero, instCharP, expand_comp_bind₁, mapAlgEquiv_trans, MonomialOrder.leadingCoeff_C, Algebra.SubmersivePresentation.aeval_invJacobianOfHasCoeffs, ker_mapAlgHom, aeval_injective_iff_of_isEmpty, WittVector.constantCoeff_wittAdd, Algebra.Generators.ofComp_kerCompPreimage, X_mem_supported, coeff_zero, eval_sub, mem_restrictDegree_iff_sup, esymmAlgHom_fin_injective, aeval_comp_bind₁, hsymm_one, weightedHomogeneousComponent_eq_zero_of_notMem, Polynomial.monic_freeMonic, rTensor_apply_monomial_tmul, IsWeightedHomogeneous.prod, eval₂_const_pUnitAlgEquiv, Algebra.Generators.repr_CotangentSpaceMap, pderiv_pow, constantCoeff_wittStructureRat_zero, WeierstrassCurve.Jacobian.map_polynomialZ, aeval_esymm_eq_multiset_esymm, supported_le_supported_iff, totalDegree_zero, MonomialOrder.coeff_pow_nsmul_degree, bind₂_C_right, MvPowerSeries.algebraMap_apply', constantCoeff_eq, LinearMap.toMvPolynomial_constantCoeff, WeierstrassCurve.Projective.map_polynomialZ, eval_rename, mkDerivationₗ_C, vars_one, StandardEtalePresentation.toPresentation_σ', totalDegree_finsetSum_le, witt_structure_prop, map_surjective, degreeOf_one, WittVector.constantCoeff_wittNSMul, LinearMap.toMvPolynomial_comp, eval₂Hom_eq_bind₂, IsHomogeneous.rename_isHomogeneous_iff, vars_bind₁, MonomialOrder.leadingCoeff_pow, WittVector.bind₁_verschiebungPoly_wittPolynomial, prod_C_add_X_eq_sum_esymm, Algebra.Presentation.instFinitePresentationModelOfHasCoeffsOfFinite, eval₂_map_comp_C, MonomialOrder.degree_pow, support_smul_eq, optionEquivRight_apply, finSuccEquiv_apply, vanishingIdeal_empty, C_eq_coe_nat, tensorEquivSum_X_tmul_X, comp_aeval_apply, vars_mul, Algebra.Presentation.relation_comp_localizationAway_inl, bind₂_comp_bind₂, WittVector.coeff_select, aeval_unique, WeierstrassCurve.Jacobian.baseChange_polynomialX, coeff_rTensorAlgHom_monomial_tmul, bind₁_bind₁, support_sum_monomial_coeff, degreeOf_mul_C_le, mem_coeffsIn_iff_coeffs_subset, esymmAlgHomMonomial_add, algebraTensorAlgEquiv_symm_map, rename_polynomial_aeval_X, weightedDecomposition.decompose'_eq, degrees_mul_eq, coeff_expand_of_not_dvd, Algebra.Generators.Hom.equivAlgHom_symm_apply_val, isHomogeneous_C_mul_X_pow, tensorEquivSum_C_tmul_one, map_iterateFrobenius_expand, vars_pow, Polynomial.toMvPolynomial_X, hsymm_zero, sumAlgEquiv_apply, Algebra.Generators.ker_comp_eq_sup, degreeOf_C_mul_le, LinearMap.polyCharpoly_map_eq_charpoly, MonomialOrder.degree_add_eq_right_of_lt, coeffsIn_eq_span_monomial, sumToIter_Xr, LinearMap.polyCharpoly_monic, Polynomial.natDegree_freeMonic, Algebra.Generators.ofComp_toAlgHom_monomial_sumElim, exists_finset_rename₂, Matrix.charpoly.univ_natDegree, WeierstrassCurve.Projective.eval_polynomial_of_Z_ne_zero, algebraMap_eq, eval_toMvPolynomial, Algebra.Presentation.algebraTensorAlgEquiv_symm_relation, coeffsIn_pow, sum_C, totalDegree_one, esymmAlgHom_apply, monomial_eq, aeval_eq_eval₂Hom, vars_C, rename_prod_mk_eval₂, AlgebraicIndependent.aevalEquivField_apply_coe, IsSymmetric.smul, aeval_C, support_map_subset, isScalarTower, toMvPowerSeries_pUnitAlgEquiv, transcendental_polynomial_aeval_X, pderiv_map, WeierstrassCurve.Jacobian.eval_polynomial, aeval_comp_expand, Algebra.Generators.naive_σ, AlgebraicIndependent.aevalEquiv_apply_coe, esymm_eq_sum_monomial, Polynomial.homogenize_monomial_of_lt, rename_C, HomogeneousSubmodule.gradedMonoid, FirstOrder.realize_genericPolyMapSurjOnOfInjOn, MvPowerSeries.coeff_mul_eq_coeff_trunc'_mul_trunc', eval₂_mul_C, StandardEtalePresentation.aeval_val_equivMvPolynomial, instFiniteOfIsEmpty, C_neg, weightedHomogeneousComponent_eq_zero, aevalTower_comp_toAlgHom, zeroLocus_vanishingIdeal_galoisConnection, coeToMvPowerSeries.ringHom_apply, restrictSupport_add, zeroLocus_span, instIsCancelMulZeroOfIsCancelAdd, coeffs_map, totalDegree_monomial_le, IsHomogeneous.rename_isHomogeneous, WittVector.polyOfInterest_vars_eq, WeierstrassCurve.Jacobian.map_polynomial, mapEquiv_trans, MvPowerSeries.WithPiTopology.tendsto_trunc'_atTop, isNoetherianRing, constantCoeff_comp_C, pderiv_inr_universalFactorizationMap_X, degrees_zero, IsHomogeneous.mul, sumAlgEquiv_symm_apply, eval₂_comp, weightedHomogeneousComponent_C_mul, MonomialOrder.leadingCoeff_zero, eval₂_pUnitAlgEquiv_symm, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, WeierstrassCurve.Jacobian.eval_polynomial_of_Z_ne_zero, dvd_C_iff_exists, Algebra.Generators.ker_eq_ker_aeval_val, instIsPushout_1, mul_monomial_mem_coeffsIn, IsHomogeneous.sum, supported_empty, C_mem_pow_idealOfVars_iff, esymmPart_zero, KaehlerDifferential.mvPolynomialBasis_repr_D, MonomialOrder.sPolynomial_monomial_mul', pderiv_eq_zero_of_notMem_vars, WittVector.map_frobeniusPoly, sum_eval_eq_zero, le_degrees_add_right, weightedTotalDegree'_zero, WittVector.constantCoeff_wittZSMul, WeierstrassCurve.Jacobian.polynomialX_eq, aeval_C_comp_left, msymm_one, C_mul_X_pow_eq_monomial, totalDegree_mul, weightedHomogeneousComponent_mem, degrees_rename_of_injective, PolynomialLaw.range_φ, coeff_add, psum_eq_mul_esymm_sub_sum, eval_C, IsWeightedHomogeneous.C_mul, mapAlgHom_apply, support_zero, Algebra.Generators.cotangentRestrict_mk, optionEquivLeft_monomial, Algebra.Generators.H1Cotangent.δ_eq_δAux, Algebra.SubmersivePresentation.ofSubsingleton_algebra_smul, MonomialOrder.leadingCoeff_mul_of_isRegular_left, KaehlerDifferential.mvPolynomialBasis_repr_comp_D, LieAlgebra.rank_eq_natTrailingDegree, WittVector.bind₁_onePoly_wittPolynomial, map_wittPolynomial, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, optionEquivLeft_symm_apply, isLocalization_C_mk', algebraTensorAlgEquiv_tmul, vars_map, mem_support_coeff_finSuccEquiv, homogeneousSubmodule_one_eq_span_X, Algebra.Generators.aeval_val_σ', eval₂Hom_id_X_eq_join₂, Algebra.Generators.Hom.toAlgHom_id, Algebra.Generators.Hom.comp_val, degreeOf_C_mul, instIsPushout, C_injective, C_mul, esymm_eq_multiset_esymm, comap_apply, vars_rename, eval₂Hom_eq_constantCoeff_of_vars, WittVector.bind₁_zero_wittPolynomial, totalDegree_finset_sum, isLocalization, instExpChar, divMonomial_monomial_mul, StandardEtalePresentation.toPresentation_val, instIsCancelAddOfIsLeftCancelAdd, sum_monomial_eq, rename_comp_bind₁, degrees_monomial_eq, zeroLocus_top, aeval_id_eq_join₁, rename_X, IsSymmetric.C, pUnitAlgEquiv_monomial, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, coeff_monomial, coeff_mul_monomial, degreeOf_zero, ringHom_ext'_iff, mem_ideal_span_monomial_image_iff_dvd, IsRegular.monomial, Matrix.charpoly.univ_map_eval₂Hom, MonomialOrder.leadingCoeff_prod_of_mem_nonZeroDivisors, comap_id_apply, aeval_one_tmul, monomial_pow, divMonomial_add_modMonomial_single, eval_sum, MonomialOrder.degree_prod, ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial, smul_eq_C_mul, eval₂_monomial, counitNat_C, finSuccEquiv_rename_finSuccEquiv, Algebra.Presentation.HasCoeffs.relation_mem_range_map, rename_expand, homogeneousSubmodule_one_pow, Algebra.Generators.fg_ker_of_finitePresentation, universalFactorizationMapPresentation_algebra_smul, MonomialOrder.degree_smul, Algebra.FiniteType.instMvPolynomialOfFinite, IsHomogeneous.sum_X_mul_pderiv, derivation_C_mul, aeval_sumElim_pderiv_inl, monomial_one_dvd_monomial_one, AnalyticAt.aeval_mvPolynomial, mul_monomial_modMonomial, eval₂_natCast, tensorEquivSum_one_tmul_X, LinearMap.polyCharpoly_coeff_eq_zero_iff_of_basis, iterToSum_C_C, mapEquiv_refl, totalDegree_sub_C_le, coeffAddMonoidHom_apply, coeff_X_mul, supported_univ, isSymmetric_rename, one_coeffsIn, mkDerivationₗ_X, universalFactorizationMap_freeMonic, Algebra.Generators.Hom.toAlgHom_monomial, Polynomial.homogenize_zero, le_degrees_add_left, irreducible_of_totalDegree_eq_one, universalFactorizationMapPresentation_val, rename_comp_rename, coe_expand, aeval_sumElim, universalFactorizationMapPresentation_σ', aeval_comp_rename, LinearMap.toMvPolynomial_eval_eq_apply, KaehlerDifferential.mvPolynomialBasis_repr_symm_single, mem_symmetricSubalgebra, MonomialOrder.degree_mul_of_isRegular_left, eval₂_rename_prod_mk, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial, mapAlgHom_coe_ringHom, monomial_sum_one, bind₁_wittPolynomial_xInTermsOfW, schwartz_zippel_sum_degreeOf, isHomogeneous_C, Algebra.FinitePresentation.out, rename_leftInverse, totalDegree_smul_le, MonomialOrder.Monic.mul, Algebra.FiniteType.iff_quotient_mvPolynomial'', Algebra.Presentation.quotientEquiv_mk, esymmAlgHom_fin_bijective, esymmAlgEquiv_apply, Polynomial.homogenize_C, mem_vanishingIdeal_iff, MonomialOrder.degree_add_of_lt, mem_vanishingIdeal_singleton_iff, MonomialOrder.div, weightedTotalDegree'_eq_bot_iff, WittVector.mul_polyOfInterest_aux5, scalarRTensor_symm_apply_single, expand_zmod, aeval_zero', weightedTotalDegree_rename_of_injective, range_mapAlgHom, counit_C, WeierstrassCurve.Projective.baseChange_polynomialZ, IsHomogeneous.prod, irreducible_sumSMulXSMulY, counitNat_X, MonomialOrder.degree_X_add_C, eval₂Hom_bind₂, mem_ideal_span_monomial_image, rename_toMvPolynomial, aeval_rename, MonomialOrder.Monic.add_of_lt, isCentralScalar, WittVector.bind₁_frobeniusPolyRat_wittPolynomial, optionEquivLeft_symm_C_X, mul_X_modMonomial, bind₂_bind₂, WittVector.aeval_verschiebungPoly, eval₂Hom_bind₁, Polynomial.homogenize_X, finSuccEquiv_X_zero, degreeOf_prod_le, MonomialOrder.monic_one, degreeOf_eq_natDegree, coeff_weightedHomogeneousComponent, WeierstrassCurve.Projective.dblX_eq, MonomialOrder.coeff_mul_of_degree_add, Algebra.Presentation.baseChange_relation, esymm_zero, rTensor_apply, C_mem_coeffsIn, bind₁_X_right, coeff_rename_eq_zero, disjoint_support_monomial, MonomialOrder.coeff_mul_of_add_of_degree_le, join₂_map, eval₂Hom_C_left, transcendental_supported_polynomial_aeval_X_iff, aeval_monomial, StandardEtalePresentation.toPresentation_relation, Polynomial.toMvPolynomial_injective, Algebra.PreSubmersivePresentation.localizationAway_jacobiMatrix, coeff_eval_eq_eval_coeff, C_pow, LinearMap.polyCharpoly_natDegree, coeffs_C_subset, Algebra.PreSubmersivePresentation.ofHasCoeffs_val, IsSymmetric.add, MonomialOrder.degree_mul, MonomialOrder.degree_monomial_le, C_sub, Algebra.Generators.self_algebra_algebraMap, esymm_eq_sum_subtype, coeff_mul_monomial', MonomialOrder.Monic.prod, ringKrullDim_of_isNoetherianRing, pderiv_X_self, quotientEquivQuotientMvPolynomial_rightInverse, WittVector.mul_polyOfInterest_aux3, pderiv_C, MvPowerSeries.trunc'_one, universalFactorizationMapPresentation_jacobiMatrix, modMonomial_add_divMonomial_single, constantCoeff_xInTermsOfW, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul, C_dvd_iff_zmod, MvRatFunc.rank_eq_max_lift, aeval_prod, homogeneousSubmodule_mul, MonomialOrder.leadingCoeff_one, Matrix.toMvPolynomial_mul, Polynomial.Bivariate.pderiv_one_equivMvPolynomial, MvPowerSeries.trunc_C_mul, exists_restrict_to_vars, lcoeff_apply, wittStructureInt_rename, WittVector.constantCoeff_wittNeg, map_wittStructureInt, algebraTensorAlgEquiv_symm_monomial, restrictSupport_eq_span, constantCoeff_comp_map, FirstOrder.Ring.mvPolynomial_zeroLocus_definable, vars_add_subset, aevalTower_algebraMap, optionEquivLeft_elim_eval, esymm_one, optionEquivLeft_symm_X, SymmetricAlgebra.IsSymmetricAlgebra.mvPolynomial, renameEquiv_symm, eval₂Hom_C, counitNat_surjective, support_symmDiff_support_subset_support_add, isEmptyRingEquiv_eq_coeff_zero, sumToIter_C, X_divMonomial, WeierstrassCurve.Projective.dblX_eq', eval_expand, RingHom.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, aeval_comp_toMvPolynomial, supportedEquivMvPolynomial_symm_C, Matrix.toMvPolynomial_constantCoeff, MvPowerSeries.trunc'_map, tensorEquivSum_X_tmul_one, instIsMaximalVanishingIdealSingletonForallSet, C_inj, expand_mul_eq_comp, WeierstrassCurve.Jacobian.map_polynomialY, eval₂_pUnitAlgEquiv, eval_X, Ideal.mem_span_pow_iff_exists_isHomogeneous, Polynomial.map_map_freeMonic, MonomialOrder.degree_prod_of_regular, supported_eq_range_rename, WeierstrassCurve.Projective.dblY_of_Y_eq', IsHomogeneous.C_mul, rename_hsymm, MonomialOrder.sPolynomial_decomposition', constantCoeff_map, transcendental_supported_X, degrees_add_of_disjoint, aeval_natDegree_le, AnalyticOnNhd.eval_continuousLinearMap', scalarRTensor_apply_tmul_apply, optionEquivLeft_symm_C_C, Algebra.Generators.Hom.algebraMap_toAlgHom, coeffsIn_le, MonomialOrder.C_mul_leadingCoeff_monomial_degree, WittVector.coeff_frobenius, degreeOf_mul_X_of_ne, Algebra.Generators.comp_σ, AnalyticOnNhd.eval_mvPolynomial, support_smul, WeierstrassCurve.Projective.map_polynomialY, tensorEquivSum_C_tmul_C, IsHomogeneous.finSuccEquiv_coeff_isHomogeneous, finsum_weightedHomogeneousComponent, WeierstrassCurve.Projective.map_polynomial, eval₂_assoc, instIsDomainOfIsCancelAdd, MvPowerSeries.subst_coe, coeff_zero_one, mapEquivMonic_symm_map_algebraMap, coe_aeval_eq_eval, WeierstrassCurve.Projective.eval_polynomialY, exists_integral_inj_algHom_of_fg, instIsLocalHomRingHomC, eval₂_eq_eval_map, weightedTotalDegree_zero, Matrix.charpoly.univ_coeff_card, Polynomial.Bivariate.equivMvPolynomial_C_C, isWeightedHomogeneous_C, linearMap_ext_iff, map_X, eval_assoc, monomial_single_add, ax_grothendieck_zeroLocus, wittPolynomial_eq_sum_C_mul_X_pow, Polynomial.homogenize_one, support_X_mul, coeffs_zero, monomial_one_mul_cancel_right_iff, MonomialOrder.degree_mul', constantCoeff_wittStructureInt_zero, Polynomial.homogenizeLM_apply, Algebra.Generators.ker_naive, degreeOf_monomial_eq, vanishingIdeal_zeroLocus_eq_radical, Polynomial.homogenize_mul, MonomialOrder.leadingTerm_eq_zero_iff, instFreeMvPolynomialKaehlerDifferential, hom_bind₁, WeierstrassCurve.Jacobian.map_polynomialX, coeff_expand_zero, C_dvd_iff_map_hom_eq_zero, rank_mvPolynomial_mvPolynomial, AnalyticOnNhd.eval_continuousLinearMap, WeierstrassCurve.Jacobian.eval_polynomialZ, vars_sum_subset, isMaximal_iff_eq_vanishingIdeal_singleton, Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, degreeOf_add_le, Matrix.mvPolynomialX_mapMatrix_aeval, algebraMap_def, MonomialOrder.leadingCoeff_mul_of_mul_leadingCoeff_ne_zero, support_C, supported_eq_vars_subset, coeffs_X_mul, eval₂_comp_right, weightedHomogeneousComponent_apply, Polynomial.aeval_homogenize_of_eq_one, MonomialOrder.degree_mul_of_right_mem_nonZeroDivisors, map_eval, Polynomial.homogenize_dvd, rename_eq, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det, totalDegree_coeff_optionEquivLeft_le, derivation_ext_iff, coeff_mul, mapEquivMonic_symm_map, ringKrullDim_mvPolynomial_of_isEmpty, IsHomogeneous.pderiv, mem_ideal_span_X_image, char_dvd_card_solutions_of_fintype_sum_lt, mem_restrictTotalDegree, vars_0, isHomogeneous_X_pow, vars_add_of_disjoint, restrictTotalDegree_le_restrictDegree, Algebra.SubmersivePresentation.basisDeriv_apply, bind₁_monomial, LinearMap.polyCharpoly_coeff_eval, MonomialOrder.degree_smul_of_mem_nonZeroDivisors, coe_coeffsIn, coe_mul, mem_image_comap_C_basicOpen, continuous_eval, Algebra.Presentation.mem_ker_naive, C_eq_smul_one, vars_monomial_single, evalₗ_apply, esymmAlgHom_surjective, aevalTower_ofNat, monomial_modMonomial, WeightedHomogeneousSubmodule.gradedMonoid, esymmAlgEquiv_symm_apply, instIsPushoutFractionRingMvPolynomial_1, rename_surjective, map_id, eval₂Hom_comp_expand, Polynomial.toMvPolynomial_C, MonomialOrder.sPolynomial_mul_monomial, MonomialOrder.degree_prod_of_mem_nonZeroDivisors, MvPowerSeries.trunc'_C, MonomialOrder.degree_pow_of_pow_leadingCoeff_ne_zero, Algebra.Generators.Hom.equivAlgHom_apply_coe, decomposition.decompose'_eq, Algebra.Generators.C_mul_X_sub_one_mem_ker, universalFactorizationMapPresentation_jacobian, MonomialOrder.sPolynomial_leadingTerm_mul, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap, esymmAlgHom_injective, coeff_sum, MvPowerSeries.trunc'_C_mul, commAlgEquiv_C_X, expand_zero_apply, Polynomial.homogenize_monomial, WeierstrassCurve.Projective.negDblY_of_Y_eq', Polynomial.coeff_freeMonic, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap', renameSymmetricSubalgebra_apply_coe, Algebra.FinitePresentation.iff_quotient_mvPolynomial', monomial_dvd_monomial, coe_mapEquivMonic_comp, transcendental_supported_polynomial_aeval_X, instIsPushoutFractionRingMvPolynomial, monomial_mul_modMonomial, eval_polynomial_eval_finSuccEquiv, constantCoeff_comp_algebraMap, sumToIter_Xl, LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly, pderiv_inl_universalFactorizationMap_X, WittVector.constantCoeff_wittSub, counit_X, instFaithfulSMul, rename_id, eval₂Hom_comp_C, Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val, rTensorAlgHom_apply_eq
constantCoeff 📖	CompOp	34 math math: eval_zero', eval₂_zero'_apply, constantCoeff_rename, constantCoeff_C, 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
decidableEqMvPolynomial 📖	CompOp	2 math math: DirectSum.coeLinearMap_eq_dfinsuppSum, DirectSum.coeAddMonoidHom_eq_support_sum
distribuMulAction 📖	CompOp	1 math math: universalFactorizationMap_comp_map
inhabited 📖	CompOp	—
lcoeff 📖	CompOp	2 math math: rTensor_apply, lcoeff_apply
monomial 📖	CompOp	132 math math: 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, 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, 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', 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, 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, coeffsIn_le, MonomialOrder.C_mul_leadingCoeff_monomial_degree, Algebra.Generators.comp_σ, 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, monomial_modMonomial, MonomialOrder.sPolynomial_mul_monomial, MonomialOrder.sPolynomial_leadingTerm_mul, Polynomial.homogenize_monomial, monomial_dvd_monomial, monomial_mul_modMonomial
monomialOneHom 📖	CompOp	1 math math: monomialOneHom_apply
smulZeroClass 📖	CompOp	15 math math: isScalarTower_right, Polynomial.homogenize_smul, smul_monomial, faithfulSMul, smulCommClass, coeff_smul, smulCommClass_right, constantCoeff_smul, support_smul_eq, isScalarTower, KaehlerDifferential.mvPolynomialBasis_repr_D, KaehlerDifferential.mvPolynomialBasis_repr_comp_D, totalDegree_smul_le, isCentralScalar, support_smul
support 📖	CompOp	64 math math: 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_add, support_rename_of_injective, support_expand_subset, eval_eq', vars_eq_support_biUnion_support, finsupp_support_eq_support, support_coeff_finSuccEquiv, support_neg, eval_eq, as_sum, eval₂_eq', 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, 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_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, 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
unique 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C_0 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
C_1 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
C_add 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	Finsupp.single_add
C_apply 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero	—	—
C_dvd_iff_dvd_coeff 📖	mathematical	—	MvPolynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring commSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike C coeff	—	coeff_C_mul dvd_mul_right ext Finset.sum_congr coeff_sum coeff_monomial Finset.sum_ite_eq' MulZeroClass.mul_zero notMem_support_iff
C_eq_coe_nat 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Nat.cast_zero C_0 Nat.cast_add Nat.cast_one C_add
C_eq_smul_one 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C Algebra.toSMul algebra Algebra.id AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	C_mul' mul_one
C_eq_zero 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
C_inj 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C	—	C_injective
C_injective 📖	mathematical	—	MvPolynomial DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C	—	Finsupp.single_injective
C_mem_coeffsIn 📖	mathematical	—	MvPolynomial Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring commSemiring module SetLike.instMembership Submodule.setLike coeffsIn DFunLike.coe RingHom RingHom.instFunLike C	—	monomial_mem_coeffsIn
C_mul 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	C_mul_monomial
C_mul' 📖	mathematical	—	MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring DFunLike.coe RingHom RingHom.instFunLike C Algebra.toSMul algebra Algebra.id	—	Algebra.smul_def
C_mul_X_eq_monomial 📖	mathematical	—	MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring DFunLike.coe RingHom RingHom.instFunLike C X LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass	—	C_mul_X_pow_eq_monomial pow_one
C_mul_X_pow_eq_monomial 📖	mathematical	—	MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring DFunLike.coe RingHom RingHom.instFunLike C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass	—	zero_add monomial_add_single C_apply
C_mul_monomial 📖	mathematical	—	MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring DFunLike.coe RingHom RingHom.instFunLike C LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial	—	AddMonoidAlgebra.single_mul_single zero_add
C_ne_zero 📖	—	—	—	—	Iff.ne C_eq_zero
C_pow 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
C_surjective 📖	mathematical	—	MvPolynomial DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C	—	Finsupp.ext Finsupp.single_eq_same
X_inj 📖	mathematical	—	X	—	X_injective
X_injective 📖	mathematical	—	MvPolynomial X	—	monomial_left_injective one_ne_zero NeZero.one Finsupp.single_left_injective
X_mul_cancel_left_iff 📖	mathematical	—	MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring X	—	monomial_one_mul_cancel_left_iff
X_mul_cancel_right_iff 📖	mathematical	—	MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring X	—	monomial_one_mul_cancel_right_iff
X_mul_mem_coeffsIn 📖	mathematical	—	MvPolynomial Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring commSemiring module SetLike.instMembership Submodule.setLike coeffsIn Distrib.toMul NonUnitalNonAssocSemiring.toDistrib X	—	mul_comm
X_ne_zero 📖	—	—	—	—	ne_zero_iff coeff_X NeZero.one
X_pow_eq_monomial 📖	mathematical	—	MvPolynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring X DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	monomial_pow Finsupp.smul_single mul_one one_pow
adjoin_range_X 📖	mathematical	—	Algebra.adjoin MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id Set.range X Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	top_unique induction_on Subalgebra.algebraMap_mem Subalgebra.add_mem Subalgebra.mul_mem Algebra.subset_adjoin Set.mem_range_self
algHom_C 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C algebraMap	—	AlgHom.commutes
algHom_ext 📖	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike X	—	—	AddMonoidAlgebra.algHom_ext' Finsupp.mulHom_ext' MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass MonoidHom.ext_mnat
algHom_ext' 📖	—	AlgHom.comp MvPolynomial CommSemiring.toSemiring commSemiring algebra IsScalarTower.toAlgHom Algebra.id isScalarTower Algebra.toSMul DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule IsScalarTower.right DFunLike.coe AlgHom AlgHom.funLike X	—	—	isScalarTower IsScalarTower.right AlgHom.coe_ringHom_injective ringHom_ext' AlgHomClass.toRingHomClass AlgHom.algHomClass
algHom_ext'_iff 📖	mathematical	—	AlgHom.comp MvPolynomial CommSemiring.toSemiring commSemiring algebra IsScalarTower.toAlgHom Algebra.id isScalarTower Algebra.toSMul DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule IsScalarTower.right DFunLike.coe AlgHom AlgHom.funLike X	—	isScalarTower IsScalarTower.right algHom_ext'
algHom_ext_iff 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike X	—	algHom_ext
algebraMap_apply 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike algebraMap algebra C	—	—
algebraMap_eq 📖	mathematical	—	algebraMap MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id C	—	—
as_sum 📖	mathematical	—	Finset.sum Finsupp MulZeroClass.toZero Nat.instMulZeroClass MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring support DFunLike.coe LinearMap RingHom.id Semiring.toModule module LinearMap.instFunLike monomial coeff	—	support_sum_monomial_coeff
coe_coeffsIn 📖	mathematical	—	SetLike.coe Submodule MvPolynomial CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring commSemiring module Submodule.setLike coeffsIn setOf	—	—
coeffAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom MvPolynomial AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring AddMonoidHom.instFunLike coeffAddMonoidHom coeff	—	—
coeff_C 📖	mathematical	—	coeff DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero Finsupp.instDecidableEq NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	Finsupp.single_apply
coeff_C_mul 📖	mathematical	—	coeff MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring DFunLike.coe RingHom RingHom.instFunLike C	—	mul_def sum_C zero_add MulZeroClass.zero_mul monomial_zero Finsupp.sum_fun_zero sum_def coeff_sum Finset.sum_congr coeff_monomial Finset.sum_ite_eq' MulZeroClass.mul_zero
coeff_X 📖	mathematical	—	coeff Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass X AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	coeff_X'
coeff_X' 📖	mathematical	—	coeff X Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.single Finsupp.instDecidableEq AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	coeff_X_pow pow_one
coeff_X_mul 📖	mathematical	—	coeff Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid Finsupp.single MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring X	—	coeff_monomial_mul one_mul
coeff_X_mul' 📖	mathematical	—	coeff MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring X Finset Finset.instMembership Finsupp.support MulZeroClass.toZero Nat.instMulZeroClass Finset.decidableMem Finsupp Finsupp.tsub Nat.instAddCommMonoid Nat.instPartialOrder Nat.instCanonicallyOrderedAdd Nat.instOrderedSub Finsupp.single NonUnitalNonAssocSemiring.toMulZeroClass	—	Nat.instCanonicallyOrderedAdd Nat.instOrderedSub coeff_monomial_mul' one_mul
coeff_X_pow 📖	mathematical	—	coeff MvPolynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring X Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.single Finsupp.instDecidableEq AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	coeff_monomial Finsupp.prod_single_index pow_zero one_mul C_1 monomial_eq
coeff_add 📖	mathematical	—	coeff MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring	—	Finsupp.add_apply
coeff_mapRange 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	coeff Finsupp.mapRange Finsupp Nat.instMulZeroClass	—	—
coeff_mem_coeffs 📖	mathematical	—	Finset Finset.instMembership coeffs coeff	—	Finset.mem_image_of_mem mem_support_iff
coeff_monomial 📖	mathematical	—	coeff DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instDecidableEq NonUnitalNonAssocSemiring.toMulZeroClass	—	Finsupp.single_apply
coeff_monomial_mul 📖	mathematical	—	coeff Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial	—	AddMonoidAlgebra.single_mul_apply_aux Finsupp.instIsLeftCancelAdd AddLeftCancelSemigroup.toIsLeftCancelAdd
coeff_monomial_mul' 📖	mathematical	—	coeff MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instLE Finsupp.decidableLE Nat.instAddCommMonoid Nat.instPartialOrder Nat.instCanonicallyOrderedAdd Finsupp.tsub Nat.instOrderedSub NonUnitalNonAssocSemiring.toMulZeroClass	—	Nat.instCanonicallyOrderedAdd Nat.instOrderedSub mul_comm coeff_mul_monomial'
coeff_mul 📖	mathematical	—	coeff MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Finset.sum Finsupp MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toAddCommMonoid Finset.HasAntidiagonal.antidiagonal Finsupp.instAddMonoid Nat.instAddMonoid Finsupp.instHasAntidiagonal	—	AddMonoidAlgebra.mul_apply_antidiagonal Finset.HasAntidiagonal.mem_antidiagonal
coeff_mul_X 📖	mathematical	—	coeff Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid Finsupp.single MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring X	—	coeff_mul_monomial mul_one
coeff_mul_X' 📖	mathematical	—	coeff MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring X Finset Finset.instMembership Finsupp.support MulZeroClass.toZero Nat.instMulZeroClass Finset.decidableMem Finsupp Finsupp.tsub Nat.instAddCommMonoid Nat.instPartialOrder Nat.instCanonicallyOrderedAdd Nat.instOrderedSub Finsupp.single NonUnitalNonAssocSemiring.toMulZeroClass	—	Nat.instCanonicallyOrderedAdd Nat.instOrderedSub coeff_mul_monomial' mul_one
coeff_mul_monomial 📖	mathematical	—	coeff Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial	—	AddMonoidAlgebra.mul_single_apply_aux Finsupp.instIsRightCancelAdd AddRightCancelSemigroup.toIsRightCancelAdd
coeff_mul_monomial' 📖	mathematical	—	coeff MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instLE Finsupp.decidableLE Nat.instAddCommMonoid Nat.instPartialOrder Nat.instCanonicallyOrderedAdd Finsupp.tsub Nat.instOrderedSub NonUnitalNonAssocSemiring.toMulZeroClass	—	Nat.instCanonicallyOrderedAdd Nat.instOrderedSub coeff_mul_monomial tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Finsupp.instCanonicallyOrderedAddOfAddLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Finsupp.isOrderedAddMonoid Finsupp.orderedSub Mathlib.Tactic.Contrapose.contrapose₂ Finset.add_subset_add_left support_monomial_subset support_mul mem_support_iff le_add_left le_rfl
coeff_one 📖	mathematical	—	coeff MvPolynomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero Finsupp.instDecidableEq NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	coeff_C
coeff_single_X 📖	mathematical	—	coeff Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass X AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	pow_one coeff_single_X_pow
coeff_single_X_pow 📖	mathematical	—	coeff Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass MvPolynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring X AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	coeff_X_pow
coeff_smul 📖	mathematical	—	coeff MvPolynomial SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring smulZeroClass	—	Finsupp.smul_apply
coeff_sum 📖	mathematical	—	coeff Finset.sum MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring	—	map_sum AddMonoidHom.instAddMonoidHomClass
coeff_zero 📖	mathematical	—	coeff MvPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring	—	—
coeff_zero_C 📖	mathematical	—	coeff Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C	—	Finsupp.single_eq_same
coeff_zero_X 📖	mathematical	—	coeff Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero X NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Finsupp.single_eq_of_ne' Finsupp.single_eq_zero
coeff_zero_one 📖	mathematical	—	coeff Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero MvPolynomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring	—	coeff_zero_C
coeffsIn_eq_span_monomial 📖	mathematical	—	coeffsIn Submodule.span MvPolynomial CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring commSemiring module setOf Submodule SetLike.instMembership Submodule.setLike Finsupp MulZeroClass.toZero Nat.instMulZeroClass DFunLike.coe LinearMap RingHom.id Semiring.toModule LinearMap.instFunLike monomial	—	le_antisymm as_sum sum_mem Submodule.addSubmonoidClass Submodule.subset_span Submodule.span_le coeff_monomial AddSubmonoidClass.toZeroMemClass
coeffsIn_le 📖	mathematical	—	Submodule MvPolynomial CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring commSemiring module Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder coeffsIn SetLike.instMembership Submodule.setLike DFunLike.coe LinearMap RingHom.id Semiring.toModule LinearMap.instFunLike monomial	—	coeffsIn_eq_span_monomial forall_swap
coeffsIn_mul 📖	mathematical	—	coeffsIn Algebra.toModule CommSemiring.toSemiring Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule.mul IsScalarTower.right MvPolynomial commSemiring module algebra	—	le_antisymm IsScalarTower.right coeffsIn_le Submodule.mul_induction_on' add_zero monomial_mul Submodule.mul_mem_mul map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Submodule.addSubmonoidClass Submodule.mul_le coeff_mul sum_mem
coeffsIn_pow 📖	mathematical	—	coeffsIn Algebra.toModule CommSemiring.toSemiring Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring MvPolynomial commSemiring module Submodule.instPowNat IsScalarTower.right algebra	—	IsScalarTower.right pow_one pow_succ coeffsIn_mul
coeffs_C 📖	mathematical	—	coeffs DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C Finset MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finset.instEmptyCollection Finset.instSingleton	—	Finset.ext coeff_C C_0
coeffs_C_subset 📖	mathematical	—	Finset Finset.instHasSubset coeffs DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C Finset.instSingleton	—	coeffs_C Finset.instReflSubset
coeffs_X_mul 📖	mathematical	—	coeffs MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring X	—	Finset.ext Finsupp.instIsLeftCancelAdd AddLeftCancelSemigroup.toIsLeftCancelAdd support_X_mul coeff_X_mul
coeffs_add 📖	mathematical	Disjoint Finset Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset.partialOrder Finset.instOrderBot support	coeffs MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Finset.instUnion	—	Finset.ext coeff_add notMem_support_iff Disjoint.notMem_of_mem_left_finset mem_support_iff Disjoint.notMem_of_mem_right_finset zero_add add_zero
coeffs_eq_empty_of_subsingleton 📖	mathematical	—	coeffs Finset Finset.instEmptyCollection	—	Subsingleton.eq_zero Unique.instSubsingleton
coeffs_mul_X 📖	mathematical	—	coeffs MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring X	—	Finset.ext Finsupp.instIsRightCancelAdd AddRightCancelSemigroup.toIsRightCancelAdd support_mul_X coeff_mul_X
coeffs_one 📖	mathematical	—	Finset Finset.instHasSubset coeffs MvPolynomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Finset.instSingleton	—	coeffs.eq_1 Finset.image_subset_iff coeff_one
coeffs_one_of_nontrivial 📖	mathematical	—	coeffs MvPolynomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Finset Finset.instSingleton	—	Finset.Subset.antisymm coeffs_one coeff_zero_one NeZero.one
coeffs_zero 📖	mathematical	—	coeffs MvPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Finset Finset.instEmptyCollection	—	—
constantCoeff_C 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike constantCoeff C	—	coeff_C
constantCoeff_X 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike constantCoeff X MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	coeff_zero_X
constantCoeff_comp_C 📖	mathematical	—	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring constantCoeff C RingHom.id	—	RingHom.ext constantCoeff_C
constantCoeff_comp_algebraMap 📖	mathematical	—	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring constantCoeff algebraMap algebra Algebra.id RingHom.id	—	constantCoeff_comp_C
constantCoeff_eq 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike constantCoeff coeff Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero	—	—
constantCoeff_monomial 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike constantCoeff LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero Finsupp.instDecidableEq NonUnitalNonAssocSemiring.toMulZeroClass	—	constantCoeff_eq coeff_monomial
constantCoeff_smul 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike constantCoeff SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring smulZeroClass	—	—
disjoint_support_monomial 📖	mathematical	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset Finset.instMembership support	Disjoint Finset.partialOrder Finset.instOrderBot DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial	—	support_monomial notMem_support_iff
eq_C_of_isEmpty 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C coeff Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero	—	C_surjective IsEmpty.instSubsingleton coeff_C
eq_zero_iff 📖	mathematical	—	MvPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring coeff	—	ext_iff
exists_coeff_ne_zero 📖	—	—	—	—	ne_zero_iff
ext 📖	—	coeff	—	—	Finsupp.ext
ext_iff 📖	mathematical	—	coeff	—	ext
faithfulSMul 📖	mathematical	—	FaithfulSMul MvPolynomial SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring smulZeroClass	—	AddMonoidAlgebra.faithfulSMul
finsupp_support_eq_support 📖	mathematical	—	Finsupp.support Finsupp MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring support	—	—
hom_eq_hom 📖	—	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring C DFunLike.coe RingHom RingHom.instFunLike X	—	—	RingHom.congr_fun ringHom_ext'
induction_on 📖	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul X	—	—	induction_on''
induction_on' 📖	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	—	Finsupp.induction monomial_zero
induction_on'' 📖	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial Distrib.toMul X	—	—	monomial_add_induction_on induction_on_monomial
induction_on_monomial 📖	mathematical	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring X	LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial	—	Finsupp.induction pow_zero mul_one pow_succ mul_assoc add_comm monomial_add_single
infinite_of_infinite 📖	mathematical	—	Infinite MvPolynomial	—	Infinite.of_injective C_injective
infinite_of_nonempty 📖	mathematical	—	Infinite MvPolynomial	—	Infinite.of_injective instInfiniteNat monomial_left_injective one_ne_zero NeZero.one Finsupp.single_injective
instIsCancelMulZeroOfIsCancelAdd 📖	mathematical	—	IsCancelMulZero MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	AddMonoidAlgebra.instIsCancelAddZeroOfIsCancelAddOfUniqueSums instUniqueSumsFinsupp TwoUniqueSums.toUniqueSums TwoUniqueSums.of_covariant_left AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
instIsDomainOfIsCancelAdd 📖	mathematical	—	IsDomain MvPolynomial CommSemiring.toSemiring commSemiring	—	instIsCancelMulZeroOfIsCancelAdd IsDomain.toIsCancelMulZero nontrivial_of_nontrivial IsDomain.toNontrivial
instNoZeroDivisors 📖	mathematical	—	NoZeroDivisors MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	AddMonoidAlgebra.instNoZeroDivisorsOfUniqueSums instUniqueSumsFinsupp TwoUniqueSums.toUniqueSums TwoUniqueSums.of_covariant_left AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
isCentralScalar 📖	mathematical	—	IsCentralScalar MvPolynomial SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring smulZeroClass MulOpposite	—	AddMonoidAlgebra.isCentralScalar
isRegular_X 📖	mathematical	—	IsRegular MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring X	—	ext coeff_X_mul IsLeftRegular.right_of_commute Commute.all
isRegular_X_pow 📖	mathematical	—	IsRegular MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X	—	IsRegular.pow isRegular_X
isRegular_prod_X 📖	mathematical	—	IsRegular MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Finset.prod CommSemiring.toCommMonoid X	—	IsRegular.prod isRegular_X
isScalarTower 📖	mathematical	—	IsScalarTower MvPolynomial SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring smulZeroClass	—	AddMonoidAlgebra.isScalarTower
isScalarTower_right 📖	mathematical	—	IsScalarTower MvPolynomial SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Algebra.toSMul Algebra.id	—	AddMonoidAlgebra.isScalarTower_self
is_id 📖	—	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring C DFunLike.coe RingHom RingHom.instFunLike X	—	—	hom_eq_hom
lcoeff_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring module Semiring.toModule LinearMap.instFunLike lcoeff coeff	—	—
le_coeffsIn_pow 📖	mathematical	—	Submodule MvPolynomial CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring commSemiring module Algebra.toModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.instPowNat IsScalarTower.right algebra coeffsIn Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring	—	IsScalarTower.right pow_zero map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Eq.ge coeffsIn_pow
linearMap_ext 📖	—	LinearMap.comp MvPolynomial CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring commSemiring Semiring.toModule module RingHom.id RingHomCompTriple.ids monomial	—	—	RingHomCompTriple.ids Finsupp.lhom_ext'
linearMap_ext_iff 📖	mathematical	—	LinearMap.comp MvPolynomial CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring commSemiring Semiring.toModule module RingHom.id RingHomCompTriple.ids monomial	—	RingHomCompTriple.ids linearMap_ext
mem_coeffsIn 📖	mathematical	—	MvPolynomial Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring commSemiring module SetLike.instMembership Submodule.setLike coeffsIn coeff	—	—
mem_coeffsIn_iff_coeffs_subset 📖	mathematical	—	MvPolynomial Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring commSemiring module SetLike.instMembership Submodule.setLike coeffsIn Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike coeffs	—	Finset.coe_image Submodule.zero_mem
mem_coeffs_iff 📖	mathematical	—	Finset Finset.instMembership coeffs Finsupp MulZeroClass.toZero Nat.instMulZeroClass support coeff	—	Finset.mem_image
mem_support_iff 📖	mathematical	—	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset Finset.instMembership support	—	—
monic_monomial_eq 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finsupp.prod MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toCommMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X	—	monomial_eq one_mul
monomialOneHom_apply 📖	mathematical	—	DFunLike.coe MonoidHom Multiplicative Finsupp MulZeroClass.toZero Nat.instMulZeroClass MvPolynomial MulOneClass.toMulOne Multiplicative.mulOneClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring MonoidHom.instFunLike monomialOneHom LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
monomial_add_induction_on 📖	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial	—	—	Finsupp.induction C_0
monomial_add_single 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid Finsupp.single Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X	—	X_pow_eq_monomial monomial_mul mul_one
monomial_eq 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike C Finsupp.prod MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toCommMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X	—	X_pow_eq_monomial Finsupp.sum_single
monomial_eq_monomial_iff 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Finsupp.single_eq_single_iff
monomial_eq_zero 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Finsupp.single_eq_zero
monomial_finsupp_sum_index 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial Finsupp.sum Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike C Finsupp.prod CommSemiring.toCommMonoid AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	monomial_sum_index
monomial_left_inj 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial	—	—
monomial_left_injective 📖	mathematical	—	Finsupp MulZeroClass.toZero Nat.instMulZeroClass MvPolynomial DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial	—	Finsupp.single_left_injective
monomial_mem_coeffsIn 📖	mathematical	—	MvPolynomial Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring commSemiring module SetLike.instMembership Submodule.setLike coeffsIn DFunLike.coe LinearMap RingHom.id Semiring.toModule LinearMap.instFunLike monomial	—	coeff_monomial AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass
monomial_mul 📖	mathematical	—	MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid	—	AddMonoidAlgebra.single_mul_single
monomial_mul_mem_coeffsIn 📖	mathematical	—	MvPolynomial Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring commSemiring module SetLike.instMembership Submodule.setLike coeffsIn Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe LinearMap RingHom.id Semiring.toModule LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	mul_comm
monomial_one_mul_cancel_left_iff 📖	mathematical	—	MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	IsRegular.left IsRegular.monomial isRegular_one
monomial_one_mul_cancel_right_iff 📖	mathematical	—	MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	IsRegular.right IsRegular.monomial isRegular_one
monomial_pow 📖	mathematical	—	MvPolynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instNatSMul Nat.instAddMonoid	—	AddMonoidAlgebra.single_pow
monomial_single_add 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid Finsupp.single Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X	—	X_pow_eq_monomial monomial_mul one_mul
monomial_sum_index 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial Finset.sum Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike C Finset.prod CommSemiring.toCommMonoid AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	monomial_sum_one C_mul' LinearMap.map_smul smul_eq_mul mul_one
monomial_sum_one 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial Finset.sum Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.prod CommSemiring.toCommMonoid	—	map_prod MonoidHom.instMonoidHomClass
monomial_zero 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Finsupp.single_zero
monomial_zero' 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero RingHom RingHom.instFunLike C	—	—
mul_X_mem_coeffsIn 📖	mathematical	—	MvPolynomial Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring commSemiring module SetLike.instMembership Submodule.setLike coeffsIn Distrib.toMul NonUnitalNonAssocSemiring.toDistrib X	—	mul_monomial_mem_coeffsIn
mul_def 📖	mathematical	—	MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Finsupp.sum Finsupp MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe LinearMap RingHom.id Semiring.toModule module LinearMap.instFunLike monomial Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid	—	AddMonoidAlgebra.mul_def
mul_monomial_mem_coeffsIn 📖	mathematical	—	MvPolynomial Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring commSemiring module SetLike.instMembership Submodule.setLike coeffsIn Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe LinearMap RingHom.id Semiring.toModule LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Nat.instCanonicallyOrderedAdd Nat.instOrderedSub coeff_mul_monomial' covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Finsupp.isOrderedAddMonoid Nat.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT Finsupp.instIsRightCancelAdd AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLT Finsupp.isOrderedCancelAddMonoid Nat.instIsOrderedCancelAddMonoid Finsupp.instCanonicallyOrderedAddOfAddLeftMono add_tsub_cancel_right Finsupp.orderedSub Finsupp.addLeftReflectLE IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le mul_one AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass
ne_zero_iff 📖	—	—	—	—	eq_zero_iff Mathlib.Tactic.Push.not_forall_eq
nontrivial_of_nontrivial 📖	mathematical	—	Nontrivial MvPolynomial	—	AddMonoidAlgebra.nontrivial
notMem_support_iff 📖	mathematical	—	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset Finset.instMembership support coeff NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	—
one_coeffsIn 📖	mathematical	—	MvPolynomial Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring commSemiring module SetLike.instMembership Submodule.setLike coeffsIn AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	C_mem_coeffsIn
one_def 📖	mathematical	—	MvPolynomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero	—	—
prod_X_pow_eq_monomial 📖	mathematical	—	Finset.prod MvPolynomial CommSemiring.toCommMonoid commSemiring Finsupp.support MulZeroClass.toZero Nat.instMulZeroClass Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring X DFunLike.coe Finsupp Finsupp.instFunLike LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	monomial_eq map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Finset.prod_congr one_mul
ringHom_ext 📖	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C X	—	—	AddMonoidAlgebra.ringHom_ext' RingHom.ext Finsupp.mulHom_ext' MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MonoidHom.ext_mnat
ringHom_ext' 📖	—	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring C DFunLike.coe RingHom RingHom.instFunLike X	—	—	ringHom_ext RingHom.ext_iff
ringHom_ext'_iff 📖	mathematical	—	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring C DFunLike.coe RingHom RingHom.instFunLike X	—	ringHom_ext'
single_eq_monomial 📖	mathematical	—	Finsupp.single Finsupp MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid commSemiring Semiring.toModule module LinearMap.instFunLike monomial	—	—
smulCommClass 📖	mathematical	—	SMulCommClass MvPolynomial SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring smulZeroClass	—	AddMonoidAlgebra.smulCommClass
smulCommClass_right 📖	mathematical	—	SMulCommClass MvPolynomial SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Algebra.toSMul Algebra.id	—	AddMonoidAlgebra.smulCommClass_self
smul_eq_C_mul 📖	mathematical	—	MvPolynomial Algebra.toSMul CommSemiring.toSemiring commSemiring algebra Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe RingHom RingHom.instFunLike C	—	C_mul'
smul_monomial 📖	mathematical	—	MvPolynomial SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring smulZeroClass DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial	—	Finsupp.smul_single
sum_C 📖	mathematical	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Finsupp.sum DFunLike.coe RingHom MvPolynomial commSemiring RingHom.instFunLike C	—	sum_monomial_eq
sum_def 📖	mathematical	—	Finsupp.sum Finsupp MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.sum support coeff	—	Finset.sum_congr
sum_monomial_eq 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Finsupp.sum Finsupp Nat.instMulZeroClass DFunLike.coe LinearMap RingHom.id MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid commSemiring Semiring.toModule module LinearMap.instFunLike monomial	—	Finsupp.sum_single_index
support_C 📖	mathematical	—	support DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike C Finset Finsupp MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finset.instEmptyCollection Finset.instSingleton Finsupp.instZero	—	support_monomial
support_X 📖	mathematical	—	support X Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset Finset.instSingleton Finsupp.single	—	X.eq_1 support_monomial one_ne_zero NeZero.one
support_X_mul 📖	mathematical	—	support MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring X Finset.map Finsupp MulZeroClass.toZero Nat.instMulZeroClass addLeftEmbedding Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid Finsupp.instIsLeftCancelAdd AddLeftCancelSemigroup.toIsLeftCancelAdd AddLeftCancelMonoid.toAddLeftCancelSemigroup AddCancelCommMonoid.toAddLeftCancelMonoid Nat.instAddCancelCommMonoid Finsupp.single	—	AddMonoidAlgebra.support_single_mul Finsupp.instIsLeftCancelAdd AddLeftCancelSemigroup.toIsLeftCancelAdd one_mul
support_X_pow 📖	mathematical	—	support MvPolynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring X Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset Finset.instSingleton Finsupp.single	—	X_pow_eq_monomial support_monomial one_ne_zero' NeZero.one
support_add 📖	mathematical	—	Finset Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset.instHasSubset support MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Finset.instUnion Finsupp.instDecidableEq	—	Finsupp.support_add
support_eq_empty 📖	mathematical	—	support Finset Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset.instEmptyCollection MvPolynomial NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring	—	Finsupp.support_eq_empty
support_monomial 📖	mathematical	—	support DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial Finset Finsupp MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toMulZeroClass Finset.instEmptyCollection Finset.instSingleton	—	—
support_monomial_subset 📖	mathematical	—	Finset Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset.instHasSubset support DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial Finset.instSingleton	—	Finsupp.support_single_subset
support_mul 📖	mathematical	—	Finset Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset.instHasSubset support MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Finset.add Finsupp.instDecidableEq Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid	—	AddMonoidAlgebra.support_mul
support_mul_X 📖	mathematical	—	support MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring X Finset.map Finsupp MulZeroClass.toZero Nat.instMulZeroClass addRightEmbedding Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid Finsupp.instIsRightCancelAdd AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Finsupp.single	—	AddMonoidAlgebra.support_mul_single Finsupp.instIsRightCancelAdd AddRightCancelSemigroup.toIsRightCancelAdd mul_one
support_nonempty 📖	mathematical	—	Finset.Nonempty Finsupp MulZeroClass.toZero Nat.instMulZeroClass support	—	Finset.nonempty_iff_ne_empty support_eq_empty
support_sdiff_support_subset_support_add 📖	mathematical	—	Finset Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset.instHasSubset Finset.instSDiff Finsupp.instDecidableEq support MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring	—	coeff_add add_zero
support_smul 📖	mathematical	—	Finset Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset.instHasSubset support MvPolynomial SMulZeroClass.toSMul NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring smulZeroClass	—	Finsupp.support_smul
support_smul_eq 📖	mathematical	—	support MvPolynomial SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid	—	Finsupp.support_smul_eq
support_sum 📖	mathematical	—	Finset Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset.instHasSubset support Finset.sum MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Finset.biUnion Finsupp.instDecidableEq	—	Finsupp.support_finset_sum
support_sum_monomial_coeff 📖	mathematical	—	Finset.sum Finsupp MulZeroClass.toZero Nat.instMulZeroClass MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring support DFunLike.coe LinearMap RingHom.id Semiring.toModule module LinearMap.instFunLike monomial coeff	—	Finsupp.sum_single
support_symmDiff_support_subset_support_add 📖	mathematical	—	Finset Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset.instHasSubset symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup Finset.instLattice Finsupp.instDecidableEq Finset.instSDiff support MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring	—	symmDiff_def Finset.sup_eq_union Finset.union_subset support_sdiff_support_subset_support_add add_comm
support_zero 📖	mathematical	—	support MvPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Finset Finsupp Nat.instMulZeroClass Finset.instEmptyCollection	—	—
zero_notMem_coeffs 📖	mathematical	—	Finset Finset.instMembership coeffs MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	mem_coeffs_iff mem_support_iff

---

← Back to Index