Eval

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

Statistics

Metric	Count
Definitions aeval, aevalTower, algebraMvPolynomial, eval, eval₂, eval₂AlgHom, eval₂Hom, map, mapAlgHom	9
Theorems adjoin_eq_range, adjoin_range_eq_range_aeval, C_dvd_iff_map_hom_eq_zero, aevalTower_C, aevalTower_X, aevalTower_algebraMap, aevalTower_comp_C, aevalTower_comp_algebraMap, aevalTower_comp_toAlgHom, aevalTower_id, aevalTower_ofId, aevalTower_ofNat, aevalTower_toAlgHom, aeval_C, aeval_X, aeval_X_left, aeval_X_left_apply, aeval_def, aeval_eq_eval, aeval_eq_eval₂Hom, aeval_eq_zero, aeval_monomial, aeval_ofNat, aeval_prod, aeval_range, aeval_sum, aeval_sumElim, aeval_unique, aeval_zero, aeval_zero', algebraMap_def, coe_aeval_eq_eval, coe_coeffs_map, coe_eval₂AlgHom, coe_eval₂Hom, coeff_map, coeffs_map, comp_aeval, comp_aeval_apply, comp_eval₂Hom, constantCoeff_comp_map, constantCoeff_map, eval_C, eval_X, eval_add, eval_assoc, eval_eq, eval_eq', eval_eval₂, eval_map, eval_mem, eval_monomial, eval_mul, eval_ofNat, eval_pow, eval_prod, eval_sum, eval_zero, eval_zero', eval₂AlgHom_X, eval₂AlgHom_apply, eval₂Hom_C, eval₂Hom_X', eval₂Hom_congr, eval₂Hom_eq_zero, eval₂Hom_map_hom, eval₂Hom_monomial, eval₂Hom_smul, eval₂Hom_zero, eval₂Hom_zero', eval₂Hom_zero'_apply, eval₂Hom_zero_apply, eval₂_C, eval₂_X, eval₂_X_pow, eval₂_add, eval₂_assoc, eval₂_comp, eval₂_comp_left, eval₂_comp_right, eval₂_congr, eval₂_dvd, eval₂_eq, eval₂_eq', eval₂_eq_eval_map, eval₂_eta, eval₂_id, eval₂_map, eval₂_map_comp_C, eval₂_mem, eval₂_monomial, eval₂_mul, eval₂_mul_C, eval₂_mul_eq_zero_of_left, eval₂_mul_eq_zero_of_right, eval₂_mul_monomial, eval₂_natCast, eval₂_ofNat, eval₂_one, eval₂_pow, eval₂_prod, eval₂_sum, eval₂_zero, eval₂_zero'_apply, eval₂_zero_apply, instFaithfulSMul, instIsScalarTower, mapAlgHom_apply, mapAlgHom_coe_ringHom, mapAlgHom_id, map_C, map_X, map_aeval, map_eval, map_eval₂, map_eval₂Hom, map_id, map_injective, map_injective_iff, map_leftInverse, map_map, map_mapRange_eq_iff, map_monomial, map_ofNat, map_rightInverse, map_surjective, map_surjective_iff, mem_range_map_iff_coeffs_subset, range_mapAlgHom, smul_eval, support_map_of_injective, support_map_subset	132
Total	141

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_eq_range 📖	mathematical	—	adjoin CommSemiring.toSemiring AlgHom.range MvPolynomial Set Set.instMembership AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra id MvPolynomial.aeval	—	adjoin_range_eq_range_aeval Subtype.range_coe
adjoin_range_eq_range_aeval 📖	mathematical	—	adjoin CommSemiring.toSemiring Set.range AlgHom.range MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra id MvPolynomial.aeval	—	AlgHom.map_adjoin MvPolynomial.aeval_X

MvPolynomial

Definitions

Name	Category	Theorems
aeval 📖	CompOp	143 math math: aeval_sum, Algebra.Generators.aeval_val_surjective, aeval_X_left, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, WittVector.aeval_verschiebung_poly', aeval_algebraMap_eq_zero_iff, algebraicIndependent_iff_ker_eq_bot, WittVector.ghostComponent_apply, aeval_wittPolynomial, aeval_range, aeval_X_left_apply, Ideal.span_pow_eq_map_homogeneousSubmodule, StandardEtalePresentation.toPresentation_algebra_smul, Ideal.span_eq_map_homogeneousSubmodule, aevalTower_ofId, IntermediateField.mem_adjoin_iff, aeval_X, AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, optionEquivLeft_apply, Algebra.SubmersivePresentation.ofSubsingleton_algebra_algebraMap, aeval_eq_eval, aeval_ite_mem_eq_self, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, AlgebraicIndependent.aeval_comp_repr, map_aeval, Algebra.Generators.algebraMap_apply, expand_zero, Polynomial.aeval_homogenize_X_one, MonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure, AddMonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure, aeval_algebraMap_eq_zero_iff_of_injective, Algebra.Generators.algebraMap_eq, Algebra.SubmersivePresentation.ofSubsingleton_relation, Algebra.Generators.Hom.aeval_val, Algebra.Presentation.comp_aeval_relation_inl, WittVector.mulN_coeff, Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, Algebra.Generators.Hom.algebraMap_toAlgHom', Algebra.Generators.cotangentSpaceBasis_repr_tmul, aeval_expand, AlgebraicIndependent.lift_reprField, aeval_algebraMap_apply, Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation, Subalgebra.mvPolynomial_aeval_coe, IsLocalization.Away.mvPolynomialQuotientEquiv_apply, AlgebraicIndependent.aeval_of_algebraicIndependent, aeval_bind₁, aeval_eq_zero, AnalyticOnNhd.aeval_mvPolynomial, MvPowerSeries.aeval_coe, WittVector.IsPoly.poly, Algebra.Presentation.aeval_val_relation, aeval_def, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, mkₐ_eq_aeval, Polynomial.eval_X_toTupleMvPolynomial_zero_eq, aeval_toMvPolynomial, universalFactorizationMapPresentation_relation, Algebra.PreSubmersivePresentation.aevalDifferential_single, AlgebraicIndependent.algebraMap_aevalEquiv, aeval_id_rename, Algebra.adjoin_range_eq_range_aeval, Algebra.Generators.aeval_val_σ, mem_zeroLocus_iff, aeval_eq_constantCoeff_of_vars, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul, MvPowerSeries.substAlgHom_coe, universalFactorizationMapPresentation_algebra_algebraMap, aeval_zero, comp_aeval, IntermediateField.mem_adjoin_range_iff, WittVector.coeff_frobeniusFun, Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul, Algebra.Generators.self_algebra_smul, algebraicIndependent_iff_injective_aeval, aeval_map_algebraMap, AlgebraicIndependent.liftAlgHom_comp_reprField, LinearMap.polyCharpolyAux_map_aeval, AlgebraicIndependent.aeval_repr, IsHomogeneous.aeval, aeval_bind₂, Algebra.adjoin_eq_range, Algebra.SubmersivePresentation.aeval_jacobianOfHasCoeffs, aeval_eq_bind₁, aeval_ofNat, Algebra.Presentation.aeval_val_relationOfHasCoeffs, Algebra.SubmersivePresentation.aeval_invJacobianOfHasCoeffs, aeval_injective_iff_of_isEmpty, aeval_comp_bind₁, Algebra.Generators.repr_CotangentSpaceMap, aeval_esymm_eq_multiset_esymm, StandardEtalePresentation.toPresentation_σ', witt_structure_prop, optionEquivRight_apply, comp_aeval_apply, WittVector.coeff_select, aeval_unique, Algebra.Generators.ofComp_toAlgHom_monomial_sumElim, Algebra.Generators.aeval_val_eq_zero, esymmAlgHom_apply, aeval_eq_eval₂Hom, AlgebraicIndependent.aevalEquivField_apply_coe, aeval_C, aeval_comp_expand, AlgebraicIndependent.aevalEquiv_apply_coe, StandardEtalePresentation.aeval_val_equivMvPolynomial, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, Algebra.Generators.ker_eq_ker_aeval_val, aeval_C_comp_left, Algebra.Generators.cotangentRestrict_mk, Algebra.SubmersivePresentation.ofSubsingleton_algebra_smul, Algebra.Generators.aeval_val_σ', Algebra.Generators.Hom.comp_val, comap_apply, aeval_id_eq_join₁, aeval_one_tmul, universalFactorizationMapPresentation_algebra_smul, aeval_sumElim_pderiv_inl, AnalyticAt.aeval_mvPolynomial, aeval_sumElim, aeval_comp_rename, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, mem_vanishingIdeal_iff, mem_vanishingIdeal_singleton_iff, aeval_zero', aeval_rename, WittVector.aeval_verschiebungPoly, aeval_monomial, Algebra.Generators.self_algebra_algebraMap, aeval_prod, exists_restrict_to_vars, aeval_comp_toMvPolynomial, aevalTower_id, aeval_natDegree_le, Algebra.Generators.Hom.algebraMap_toAlgHom, WittVector.coeff_frobenius, MvPowerSeries.subst_coe, coe_aeval_eq_eval, Matrix.mvPolynomialX_mapMatrix_aeval, Polynomial.aeval_homogenize_of_eq_one, Algebra.SubmersivePresentation.basisDeriv_apply, Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val
aevalTower 📖	CompOp	11 math math: aevalTower_ofId, aevalTower_comp_C, aevalTower_toAlgHom, optionEquivRight_symm_apply, aevalTower_X, aevalTower_C, aevalTower_comp_algebraMap, aevalTower_comp_toAlgHom, aevalTower_algebraMap, aevalTower_id, aevalTower_ofNat
algebraMvPolynomial 📖	CompOp	15 math math: instIsScalarTower, instIsIntegralMvPolynomial, instIsAlgebraicMvPolynomialOfNoZeroDivisors, isIntegral_iff_isIntegral_coeff, instIsPushout_1, instIsAlgebraicMvPolynomialOfNoZeroDivisors_1, isLocalization_C_mk', instIsPushout, isLocalization, Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial, rank_mvPolynomial_mvPolynomial, algebraMap_def, instIsPushoutFractionRingMvPolynomial_1, instIsPushoutFractionRingMvPolynomial, instFaithfulSMul
eval 📖	CompOp	109 math math: funext_iff, eval_indicator_apply_eq_one, Height.logHeight_eval_ge, Ideal.mem_span_iff_exists_isHomogeneous, eval_zero', WeierstrassCurve.Projective.eval_polynomial, isEmptyRingEquiv_apply, WeierstrassCurve.Projective.polynomial_relation, AnalyticOnNhd.eval_linearMap', Polynomial.eval_eq_div_eval_toTupleMvPolynomial, WeierstrassCurve.Jacobian.eval_polynomialY, eval_map, char_dvd_card_solutions_of_add_lt, aeval_eq_eval, schwartz_zippel_totalDegree, eval_mem, ax_grothendieck_of_definable, Height.logHeight_eval_ge', eval_rename_prod_mk, eval_eval₂, eval₂_id, Height.logHeight_eval_le', FirstOrder.Ring.lift_genericPolyMap, WeierstrassCurve.Jacobian.eval_polynomialX_of_Z_ne_zero, eval_comp_toMvPolynomial, WeierstrassCurve.Jacobian.eval_polynomialX, WeierstrassCurve.Projective.eval_polynomialX, WeierstrassCurve.Jacobian.eval_polynomialY_of_Z_ne_zero, eval_ofNat, eval_eq_eval_mv_eval', WeierstrassCurve.Jacobian.polynomial_relation, LinearMap.polyCharpolyAux_map_eval, eval_prod, AnalyticOnNhd.eval_linearMap, IsNonarchimedean.eval_mvPolynomial_le, eval_eq', eval_neg, Polynomial.eval_homogenize, WeierstrassCurve.Projective.eval_polynomialX_of_Z_ne_zero, LinearMap.polyCharpolyAux_map_eq_charpoly, LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff, eval_eq, eval_add, eval_monomial, AbsoluteValue.eval_mvPolynomial_le, WeierstrassCurve.Projective.eval_polynomialZ, eval_pow, Height.mulHeight_eval_ge, eval_zero, schwartz_zippel_sup_sum, eval_mul, eval_indicator_apply_eq_zero, WeierstrassCurve.Projective.negDblY_eq, smul_eval, WeierstrassCurve.Projective.eval_polynomialY_of_Z_ne_zero, isEmptyAlgEquiv_apply, Matrix.toMvPolynomial_eval_eq_apply, funext_set_iff, char_dvd_card_solutions, char_dvd_card_solutions_of_sum_lt, Matrix.mvPolynomialX_mapMatrix_eval, Height.mulHeight_eval_le, WeierstrassCurve.Projective.negDblY_eq', LinearMap.polyCharpolyAux_coeff_eval, eval_sub, Height.logHeight_eval_le, eval_rename, LinearMap.polyCharpoly_map_eq_charpoly, WeierstrassCurve.Projective.eval_polynomial_of_Z_ne_zero, eval_toMvPolynomial, WeierstrassCurve.Jacobian.eval_polynomial, FirstOrder.realize_genericPolyMapSurjOnOfInjOn, eval₂_comp, WeierstrassCurve.Jacobian.eval_polynomial_of_Z_ne_zero, sum_eval_eq_zero, eval_C, eval_sum, LinearMap.toMvPolynomial_eval_eq_apply, schwartz_zippel_sum_degreeOf, ax_grothendieck_of_locally_finite, WeierstrassCurve.Projective.dblX_eq, ax_grothendieck_univ, coeff_eval_eq_eval_coeff, Height.mulHeight_eval_le', optionEquivLeft_elim_eval, Height.mulHeight_eval_ge', WeierstrassCurve.Projective.dblX_eq', eval_expand, eval_X, Ideal.mem_span_pow_iff_exists_isHomogeneous, WeierstrassCurve.Projective.dblY_of_Y_eq', AnalyticOnNhd.eval_continuousLinearMap', AnalyticOnNhd.eval_mvPolynomial, coe_aeval_eq_eval, WeierstrassCurve.Projective.eval_polynomialY, eval₂_eq_eval_map, eval_assoc, ax_grothendieck_zeroLocus, AnalyticOnNhd.eval_continuousLinearMap, WeierstrassCurve.Jacobian.eval_polynomialZ, map_eval, char_dvd_card_solutions_of_fintype_sum_lt, LinearMap.polyCharpoly_coeff_eval, continuous_eval, evalₗ_apply, expand_zero_apply, WeierstrassCurve.Projective.negDblY_of_Y_eq', eval_polynomial_eval_finSuccEquiv, LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly
eval₂ 📖	CompOp	67 math math: eval₂_mul_eq_zero_of_left, pUnitAlgEquiv_apply, eval₂Hom_X, MvPowerSeries.eval₂_coe, eval₂_expand, Polynomial.eval₂_homogenize_of_eq_one, eval₂_zero'_apply, MvPowerSeries.eval₂Hom_eq_extend, eval₂_pow, eval₂_prod, map_eval₂, eval_map, eval₂_zero, eval₂_ofNat, map_mvPolynomial_eq_eval₂, eval_eval₂, eval₂_id, eval₂_mul_monomial, eval₂_const_pUnitAlgEquiv_symm, eval₂_sum, eval₂_congr, eval₂_map, eval₂_neg, eval₂_X, eval₂_one, eval₂_mul_eq_zero_of_right, eval₂_C, rename_eval₂, eval₂_cast_comp, eval₂_dvd, mk_eq_eval₂, eval₂_eq', aeval_def, coe_eval₂Hom, eval₂_add, eval₂_zero_apply, eval₂_sub, eval₂_mul, eval₂_eta, eval₂_rename, quotientEquivQuotientMvPolynomial_leftInverse, eval₂_const_pUnitAlgEquiv, coe_eval₂AlgHom, eval₂_map_comp_C, rename_prod_mk_eval₂, eval₂_mul_C, eval₂_X_pow, eval₂_comp, eval₂_pUnitAlgEquiv_symm, polynomial_eval_eval₂, mapAlgHom_apply, Matrix.mvPolynomialX_map_eval₂, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, eval₂_eq, eval₂_monomial, eval₂_natCast, coe_expand, eval₂_rename_prod_mk, eval₂_mem, eval₂_comp_left, quotientEquivQuotientMvPolynomial_rightInverse, IsHomogeneous.eval₂, eval₂_pUnitAlgEquiv, eval₂_assoc, eval₂_eq_eval_map, eval_assoc, eval₂_comp_right
eval₂AlgHom 📖	CompOp	3 math math: coe_eval₂AlgHom, eval₂AlgHom_X, eval₂AlgHom_apply
eval₂Hom 📖	CompOp	46 math math: toMvPowerSeries_uniformContinuous, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply, AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop, eval₂Hom_monomial, map_eval₂Hom, comp_eval₂Hom, eval₂Hom_C_id_eq_join₁, eval₂Hom_C_eq_bind₁, eval₂Hom_comp_bind₂, map_aeval, eval₂Hom_congr, eval₂Hom_zero_apply, eval₂Hom_congr', Matrix.charpoly.univ_coeff_eval₂Hom, eval₂Hom_X', eval₂Hom_rename, eval₂Hom_zero', CommRingCat.HomTopology.mvPolynomialHomeomorph_symm_apply_hom, coe_eval₂Hom, eval₂Hom_zero'_apply, eval₂Hom_zero, eval₂Hom_map_hom, finSuccEquiv_eq, ker_eval₂Hom_universalFactorizationMap, quotientEquivQuotientMvPolynomial_leftInverse, aeval_bind₂, eval₂Hom_eq_zero, eval₂Hom_eq_bind₂, finSuccEquiv_apply, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop, aeval_eq_eval₂Hom, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom, eval₂Hom_id_X_eq_join₂, eval₂Hom_eq_constantCoeff_of_vars, Matrix.charpoly.univ_map_eval₂Hom, eval₂_C_mk_eq_zero, eval₂Hom_bind₂, eval₂Hom_bind₁, eval₂Hom_C_left, quotientEquivQuotientMvPolynomial_rightInverse, eval₂Hom_C, eval₂AlgHom_apply, hom_bind₁, eval₂Hom_smul, eval₂Hom_comp_expand, eval₂Hom_comp_C
map 📖	CompOp	108 math math: AlgebraicGeometry.AffineSpace.map_Spec_map, map_bind₁, map_mapRange_eq_iff, map_comp_C, Polynomial.homogenize_map, Matrix.charpoly.univ_map_map, universalFactorizationMap_comp_map, IsSymmetric.map, ker_map, map_leftInverse, WeierstrassCurve.Jacobian.baseChange_polynomialZ, mem_range_map_iff_coeffs_subset, exists_dvd_map_of_isAlgebraic, map_comp_rename, map_bind₂, map_eval₂, eval_map, Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs, join₂_comp_map, map_map, IsHomogeneous.map, map_expand, map_frobenius_expand, expand_char, map_rename, Algebra.Presentation.map_relationOfHasCoeffs, eval₂_map, map_esymm, WeierstrassCurve.Projective.baseChange_polynomial, Matrix.toMvPolynomial_map, bind₂_map, degrees_map_of_injective, LinearMap.polyCharpoly_baseChange, commAlgEquiv_C, mapEquiv_apply, Algebra.SubmersivePresentation.map_invJacobianOfHasCoeffs, mapAlgEquiv_apply, WittVector.frobeniusPoly_zmod, WeierstrassCurve.Jacobian.baseChange_polynomialY, map_ofNat, WeierstrassCurve.Projective.baseChange_polynomialY, LinearMap.toMvPolynomial_baseChange, coe_coeffs_map, MvPowerSeries.truncFinset_map, map_expand_pow_char, mapRange_eq_map, map_hsymm, degrees_map_le, WeierstrassCurve.Projective.map_polynomialX, Algebra.SubmersivePresentation.map_jacobianRelationsOfHasCoeffs, MvPowerSeries.trunc_map, WeierstrassCurve.Jacobian.baseChange_polynomial, universalFactorizationMapPresentation_relation, map_surjective_iff, map_injective_iff, map_injective, support_map_of_injective, AlgebraicGeometry.AffineSpace.map_SpecMap, WeierstrassCurve.Projective.baseChange_polynomialX, map_C, LinearMap.polyCharpolyAux_baseChange, map_monomial, vars_map_of_injective, aeval_map_algebraMap, eval₂Hom_map_hom, ker_eval₂Hom_universalFactorizationMap, coeff_map, map_rightInverse, killCompl_map, WeierstrassCurve.Jacobian.map_polynomialZ, WeierstrassCurve.Projective.map_polynomialZ, witt_structure_prop, map_surjective, eval₂_map_comp_C, WeierstrassCurve.Jacobian.baseChange_polynomialX, algebraTensorAlgEquiv_symm_map, map_iterateFrobenius_expand, support_map_subset, pderiv_map, coeffs_map, WeierstrassCurve.Jacobian.map_polynomial, WittVector.map_frobeniusPoly, map_wittPolynomial, algebraTensorAlgEquiv_tmul, vars_map, Algebra.Presentation.HasCoeffs.relation_mem_range_map, universalFactorizationMapPresentation_σ', mapAlgHom_coe_ringHom, WeierstrassCurve.Projective.baseChange_polynomialZ, Algebra.Presentation.baseChange_relation, join₂_map, C_dvd_iff_zmod, map_wittStructureInt, constantCoeff_comp_map, MvPowerSeries.trunc'_map, WeierstrassCurve.Jacobian.map_polynomialY, Polynomial.map_map_freeMonic, constantCoeff_map, WeierstrassCurve.Projective.map_polynomialY, WeierstrassCurve.Projective.map_polynomial, eval₂_eq_eval_map, map_X, WeierstrassCurve.Jacobian.map_polynomialX, C_dvd_iff_map_hom_eq_zero, algebraMap_def, eval₂_comp_right, map_eval, map_id
mapAlgHom 📖	CompOp	9 math math: universalFactorizationMap_comp_map, mapAlgHom_id, algebraTensorAlgEquiv_symm_comp_aeval, sumAlgEquiv_comp_rename_inl, ker_mapAlgHom, mapAlgHom_apply, mapAlgHom_coe_ringHom, range_mapAlgHom, universalFactorizationMapPresentation_jacobiMatrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C_dvd_iff_map_hom_eq_zero 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring	MvPolynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero AddMonoidAlgebra.nonUnitalSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring AddMonoid.toAddSemigroup Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike C map NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp.instAdd	—	C_dvd_iff_dvd_coeff ext_iff coeff_map
aevalTower_C 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra AlgHom.funLike aevalTower RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike C	—	eval₂_C
aevalTower_X 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra AlgHom.funLike aevalTower X	—	eval₂_X
aevalTower_algebraMap 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra AlgHom.funLike aevalTower RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap Algebra.id	—	eval₂_C
aevalTower_comp_C 📖	mathematical	—	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHomClass.toRingHom AlgHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid AddMonoidAlgebra.algebra AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass aevalTower C	—	RingHom.ext AlgHomClass.toRingHomClass AlgHom.algHomClass aevalTower_C
aevalTower_comp_algebraMap 📖	mathematical	—	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHomClass.toRingHom AlgHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid AddMonoidAlgebra.algebra AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass aevalTower algebraMap Algebra.id	—	aevalTower_comp_C
aevalTower_comp_toAlgHom 📖	mathematical	—	AlgHom.comp MvPolynomial CommSemiring.toSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra aevalTower IsScalarTower.toAlgHom Algebra.id AddMonoidAlgebra.isScalarTower 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 Algebra.toSMul IsScalarTower.right	—	AlgHom.coe_ringHom_injective AddMonoidAlgebra.isScalarTower IsScalarTower.right aevalTower_comp_algebraMap
aevalTower_id 📖	mathematical	—	aevalTower Algebra.id AlgHom.id CommSemiring.toSemiring aeval	—	algHom_ext aevalTower_X aeval_X
aevalTower_ofId 📖	mathematical	—	aevalTower Algebra.id Algebra.ofId CommSemiring.toSemiring aeval	—	algHom_ext aevalTower_X aeval_X
aevalTower_ofNat 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra AlgHom.funLike aevalTower	—	map_ofNat AlgHomClass.toRingHomClass AlgHom.algHomClass
aevalTower_toAlgHom 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra AlgHom.funLike aevalTower IsScalarTower.toAlgHom Algebra.id AddMonoidAlgebra.isScalarTower 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 Algebra.toSMul IsScalarTower.right	—	aevalTower_algebraMap
aeval_C 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike aeval RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike C algebraMap	—	eval₂_C
aeval_X 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike aeval X	—	eval₂_X
aeval_X_left 📖	mathematical	—	aeval MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.algebra CommSemiring.toSemiring Algebra.id Finsupp.instAddMonoid Nat.instAddMonoid X AlgHom.id AddMonoidAlgebra.semiring	—	aeval_unique
aeval_X_left_apply 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid AlgHom.funLike aeval X	—	AlgHom.congr_fun aeval_X_left
aeval_def 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike aeval eval₂ algebraMap	—	—
aeval_eq_eval 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike aeval RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Semiring.toNonAssocSemiring RingHom.instFunLike eval	—	—
aeval_eq_eval₂Hom 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike aeval RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Semiring.toNonAssocSemiring RingHom.instFunLike eval₂Hom algebraMap	—	—
aeval_eq_zero 📖	mathematical	Finset SetLike.instMembership Finset.instSetLike Finsupp.support MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike aeval NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	eval₂Hom_eq_zero
aeval_monomial 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike aeval LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike monomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike algebraMap Finsupp.prod CommSemiring.toCommMonoid Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	eval₂Hom_monomial
aeval_ofNat 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike aeval	—	map_ofNat AlgHomClass.toRingHomClass AlgHom.algHomClass
aeval_prod 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike aeval Finset.prod CommSemiring.toCommMonoid AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid	—	map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
aeval_range 📖	mathematical	—	AlgHom.range MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id aeval Algebra.adjoin Set.range	—	le_antisymm induction_on Subsemiring.subset_closure Set.mem_range_self aeval_C map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Subalgebra.add_mem map_mul NonUnitalAlgSemiHomClass.toMulHomClass aeval_X Subalgebra.mul_mem Algebra.subset_adjoin Algebra.adjoin_le_iff
aeval_sum 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike aeval Finset.sum AddMonoidAlgebra.addAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass
aeval_sumElim 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike aeval RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddCommMonoid.toAddMonoid X AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass C	—	induction_on algHom_C map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass aeval_X
aeval_unique 📖	mathematical	—	aeval MvPolynomial DFunLike.coe AlgHom AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike X	—	algHom_ext aeval_X
aeval_zero 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike aeval Pi.instZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring RingHom RingHom.instFunLike algebraMap AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass constantCoeff	—	eval₂Hom_zero_apply
aeval_zero' 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike aeval NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring RingHom RingHom.instFunLike algebraMap AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass constantCoeff	—	aeval_zero
algebraMap_def 📖	mathematical	—	algebraMap MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.semiring CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid algebraMvPolynomial map	—	—
coe_aeval_eq_eval 📖	mathematical	—	RingHomClass.toRingHom AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass aeval eval	—	AlgHomClass.toRingHomClass AlgHom.algHomClass
coe_coeffs_map 📖	mathematical	—	Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike coeffs DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map Set.image Semiring.toNonAssocSemiring	—	instIsConcreteLE coeffs_map
coe_eval₂AlgHom 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike eval₂AlgHom eval₂ algebraMap	—	—
coe_eval₂Hom 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval₂Hom eval₂	—	—
coeff_map 📖	mathematical	—	coeff DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map Semiring.toNonAssocSemiring	—	induction_on map_C coeff_C RingHom.map_zero RingHom.map_add coeff_add Nat.instCanonicallyOrderedAdd Nat.instOrderedSub RingHom.map_mul map_X coeff_mul_X'
coeffs_map 📖	mathematical	—	Finset Finset.instHasSubset coeffs DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map Finset.image Semiring.toNonAssocSemiring	—	induction_on'' map_C coeffs_C map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass coeffs_add disjoint_support_monomial map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass Finset.disjoint_of_subset_left support_map_subset Finset.disjoint_of_subset_right Finset.image_union Finset.union_subset_iff HasSubset.Subset.trans Finset.instIsTransSubset map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_X coeffs_mul_X
comp_aeval 📖	mathematical	—	AlgHom.comp MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id aeval DFunLike.coe AlgHom AlgHom.funLike	—	algHom_ext aeval_X
comp_aeval_apply 📖	mathematical	—	DFunLike.coe AlgHom CommSemiring.toSemiring AlgHom.funLike MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id aeval	—	comp_aeval AlgHom.coe_comp
comp_eval₂Hom 📖	mathematical	—	RingHom.comp MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring eval₂Hom DFunLike.coe RingHom RingHom.instFunLike	—	ringHom_ext' RingHom.ext eval₂_C eval₂_X eval₂Hom_X'
constantCoeff_comp_map 📖	mathematical	—	RingHom.comp MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring constantCoeff map	—	ringHom_ext' RingHom.ext map_C constantCoeff_C map_X constantCoeff_X map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
constantCoeff_map 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike constantCoeff map	—	coeff_map
eval_C 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval C	—	eval₂_C
eval_X 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval X	—	eval₂_X
eval_add 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp.instAdd NonAssocSemiring.toNonUnitalNonAssocSemiring	—	eval₂_add
eval_assoc 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval eval₂ AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid C	—	eval₂_comp_left RingHom.ext eval₂_C
eval_eq 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring support Distrib.toMul NonUnitalNonAssocSemiring.toDistrib coeff Finset.prod CommSemiring.toCommMonoid Finsupp.support Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Finsupp.instFunLike	—	—
eval_eq' 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring support Distrib.toMul NonUnitalNonAssocSemiring.toDistrib coeff Finset.prod CommSemiring.toCommMonoid Finset.univ Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Finsupp.instFunLike	—	eval₂_eq'
eval_eval₂ 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval eval₂ AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid RingHom.comp	—	induction_on eval₂_C eval₂_add map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass eval₂_mul eval₂_X map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass
eval_map 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval map eval₂	—	induction_on map_C eval_C eval₂_C map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass eval₂_add map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_X eval_X eval₂_mul eval₂_X
eval_mem 📖	mathematical	SetLike.instMembership coeff	SetLike.instMembership DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval	—	eval₂_mem
eval_monomial 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike monomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Finsupp.prod CommSemiring.toCommMonoid Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	eval₂_monomial
eval_mul 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval AddMonoidAlgebra.instMul Finsupp.instAdd Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	eval₂_mul
eval_ofNat 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval	—	map_ofNat RingHom.instRingHomClass
eval_pow 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp.instAddMonoid	—	eval₂_pow
eval_prod 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval Finset.prod CommSemiring.toCommMonoid AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid	—	map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
eval_sum 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval Finset.sum AddMonoidAlgebra.addAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring	—	map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
eval_zero 📖	mathematical	—	eval Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring constantCoeff	—	eval₂Hom_zero
eval_zero' 📖	mathematical	—	eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring constantCoeff	—	eval₂Hom_zero
eval₂AlgHom_X 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike eval₂AlgHom X	—	eval₂_X
eval₂AlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike eval₂AlgHom RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Semiring.toNonAssocSemiring RingHom.instFunLike eval₂Hom algebraMap	—	—
eval₂Hom_C 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval₂Hom C	—	eval₂_C
eval₂Hom_X' 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval₂Hom X	—	eval₂_X
eval₂Hom_congr 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval₂Hom	—	—
eval₂Hom_eq_zero 📖	mathematical	Finset SetLike.instMembership Finset.instSetLike Finsupp.support MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval₂Hom NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	as_sum map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Finset.sum_eq_zero Finsupp.mem_support_iff eval₂Hom_monomial Finsupp.prod.eq_1 Finset.prod_eq_zero zero_pow MulZeroClass.mul_zero
eval₂Hom_map_hom 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval₂Hom map RingHom.comp	—	eval₂_map
eval₂Hom_monomial 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval₂Hom LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike monomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Finsupp.prod CommSemiring.toCommMonoid Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	monomial_eq Finset.prod_congr map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass eval₂Hom_C map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_pow eval₂Hom_X'
eval₂Hom_smul 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval₂Hom Algebra.toSMul AddMonoidAlgebra.semiring Finsupp.instAddMonoid AddMonoidAlgebra.algebra Algebra.id	—	smul_eq_C_mul eval₂_mul eval₂_C
eval₂Hom_zero 📖	mathematical	—	eval₂Hom Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.comp MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp Nat.instMulZeroClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid constantCoeff	—	ringHom_ext' RingHom.ext eval₂_C constantCoeff_C eval₂Hom_X' constantCoeff_X map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
eval₂Hom_zero' 📖	mathematical	—	eval₂Hom MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.comp MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp Nat.instMulZeroClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid constantCoeff	—	eval₂Hom_zero
eval₂Hom_zero'_apply 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval₂Hom NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring constantCoeff	—	eval₂Hom_zero_apply
eval₂Hom_zero_apply 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval₂Hom Pi.instZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring constantCoeff	—	RingHom.congr_fun eval₂Hom_zero
eval₂_C 📖	mathematical	—	eval₂ DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike C	—	C_apply eval₂_monomial Finsupp.prod_zero_index mul_one
eval₂_X 📖	mathematical	—	eval₂ X	—	eval₂_monomial RingHom.map_one Finsupp.prod_single_index pow_zero pow_one one_mul
eval₂_X_pow 📖	mathematical	—	eval₂ MvPolynomial Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid X	—	X_pow_eq_monomial eval₂_monomial map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Finsupp.prod_single_index pow_zero one_mul
eval₂_add 📖	mathematical	—	eval₂ MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	Finsupp.sum_add_index RingHom.map_zero MulZeroClass.zero_mul RingHom.map_add add_mul Distrib.rightDistribClass
eval₂_assoc 📖	mathematical	—	eval₂ MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid C	—	eval₂_comp_left RingHom.ext eval₂_C
eval₂_comp 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid eval eval₂	—	map_id eval_map eval₂_comp_right
eval₂_comp_left 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike eval₂ RingHom.comp	—	induction_on eval₂_C eval₂_add RingHom.map_add eval₂_mul eval₂_X RingHom.map_mul
eval₂_comp_right 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike eval₂ MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid map	—	induction_on eval₂_C map_C eval₂_add RingHom.map_add eval₂_mul RingHom.map_mul map_X eval₂_X
eval₂_congr 📖	mathematical	—	eval₂	—	Finset.sum_congr Finset.prod_congr Finsupp.mem_support_iff
eval₂_dvd 📖	mathematical	MvPolynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero AddMonoidAlgebra.nonUnitalSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring AddMonoid.toAddSemigroup Finsupp.instAddMonoid Nat.instAddMonoid	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring eval₂	—	map_dvd NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass
eval₂_eq 📖	mathematical	—	eval₂ Finset.sum Finsupp MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring support Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe RingHom RingHom.instFunLike coeff Finset.prod CommSemiring.toCommMonoid Finsupp.support Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Finsupp.instFunLike	—	—
eval₂_eq' 📖	mathematical	—	eval₂ Finset.sum Finsupp MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring support Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe RingHom RingHom.instFunLike coeff Finset.prod CommSemiring.toCommMonoid Finset.univ Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Finsupp.instFunLike	—	Finset.sum_congr
eval₂_eq_eval_map 📖	mathematical	—	eval₂ DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval map	—	eval₂_comp_left RingHom.ext eval₂_C RingHomCompTriple.comp_apply RingHomCompTriple.right_ids eval₂_X
eval₂_eta 📖	mathematical	—	eval₂ MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid C X	—	induction_on eval₂_C eval₂_add eval₂_mul eval₂_X
eval₂_id 📖	mathematical	—	eval₂ RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike eval	—	—
eval₂_map 📖	mathematical	—	eval₂ DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map RingHom.comp Semiring.toNonAssocSemiring	—	eval_map map_map
eval₂_map_comp_C 📖	mathematical	—	eval₂ MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid map C DFunLike.coe RingHom RingHom.instFunLike	—	induction_on eval₂_C map_C eval₂_add map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass eval₂_mul eval₂_X map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_X
eval₂_mem 📖	mathematical	SetLike.instMembership DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike coeff	SetLike.instMembership eval₂	—	notMem_support_iff RingHom.map_zero ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass monomial_add_induction_on eval₂_C coeff_C eval₂_add eval₂_monomial AddMemClass.add_mem AddSubmonoidClass.toAddMemClass MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubsemiringClass.toSubmonoidClass coeff_add coeff_monomial add_zero prod_mem pow_mem map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass zero_add
eval₂_monomial 📖	mathematical	—	eval₂ DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike monomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike Finsupp.prod CommSemiring.toCommMonoid Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Finsupp.sum_single_index RingHom.map_zero MulZeroClass.zero_mul
eval₂_mul 📖	mathematical	—	eval₂ MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	induction_on eval₂_mul_C eval₂_C mul_add Distrib.leftDistribClass eval₂_add eval₂_mul_monomial map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_one Finsupp.prod_single_index pow_zero pow_one
eval₂_mul_C 📖	mathematical	—	eval₂ MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass RingHom.instFunLike C Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	eval₂_mul_monomial mul_one
eval₂_mul_eq_zero_of_left 📖	mathematical	eval₂ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	eval₂ MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	eval₂_mul MulZeroClass.zero_mul
eval₂_mul_eq_zero_of_right 📖	mathematical	eval₂ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	eval₂ MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	eval₂_mul MulZeroClass.mul_zero
eval₂_mul_monomial 📖	mathematical	—	eval₂ MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike monomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike Finsupp.prod CommSemiring.toCommMonoid Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	induction_on C_mul_monomial eval₂_monomial RingHom.map_mul eval₂_C add_mul Distrib.rightDistribClass eval₂_add monomial_single_add pow_one mul_assoc Finsupp.prod_add_index pow_zero pow_add Finsupp.prod_single_index mul_left_comm RingHom.map_one mul_one
eval₂_natCast 📖	mathematical	—	eval₂ MvPolynomial AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring	—	eval₂_C map_natCast RingHom.instRingHomClass
eval₂_ofNat 📖	mathematical	—	eval₂	—	eval₂_natCast
eval₂_one 📖	mathematical	—	eval₂ MvPolynomial AddMonoidAlgebra.zero Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instZero AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	eval₂_C RingHom.map_one
eval₂_pow 📖	mathematical	—	eval₂ MvPolynomial Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid	—	pow_zero eval₂_one pow_add pow_one eval₂_mul
eval₂_prod 📖	mathematical	—	eval₂ Finset.prod MvPolynomial CommSemiring.toCommMonoid AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid	—	map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
eval₂_sum 📖	mathematical	—	eval₂ Finset.sum MvPolynomial AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
eval₂_zero 📖	mathematical	—	eval₂ MvPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	Finsupp.sum_zero_index
eval₂_zero'_apply 📖	mathematical	—	eval₂ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe RingHom RingHom.instFunLike MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp Nat.instMulZeroClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid constantCoeff	—	eval₂_zero_apply
eval₂_zero_apply 📖	mathematical	—	eval₂ Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe RingHom RingHom.instFunLike MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp Nat.instMulZeroClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid constantCoeff	—	eval₂Hom_zero_apply
instFaithfulSMul 📖	mathematical	—	FaithfulSMul MvPolynomial Algebra.toSMul AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.semiring CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid algebraMvPolynomial	—	faithfulSMul_iff_algebraMap_injective map_injective FaithfulSMul.algebraMap_injective
instIsScalarTower 📖	mathematical	—	IsScalarTower MvPolynomial Algebra.toSMul AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid algebraMvPolynomial	—	IsScalarTower.of_algebraMap_eq' RingHom.ext ext map_C
mapAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra AlgHom.funLike mapAlgHom eval₂ AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid RingHom.comp Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass C RingHomClass.toRingHom X	—	—
mapAlgHom_coe_ringHom 📖	mathematical	—	RingHomClass.toRingHom AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra AlgHom.funLike AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass AlgHomClass.toRingHomClass AlgHom.algHomClass mapAlgHom map Semiring.toNonAssocSemiring	—	RingHom.mk_coe AlgHomClass.toRingHomClass AlgHom.algHomClass
mapAlgHom_id 📖	mathematical	—	mapAlgHom AlgHom.id CommSemiring.toSemiring MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra	—	AlgHom.ext map_id
map_C 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map Semiring.toNonAssocSemiring C	—	map_monomial
map_X 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map X	—	eval₂_X
map_aeval 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike aeval AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass eval₂Hom RingHom.comp algebraMap	—	comp_eval₂Hom
map_eval 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid eval map	—	eval₂_eq_eval_map eval₂_id eval₂_comp_right map_id
map_eval₂ 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map eval₂ AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid C	—	induction_on eval₂_C map_C eval₂_add RingHom.map_add eval₂_mul RingHom.map_mul map_X eval₂_X
map_eval₂Hom 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid eval₂Hom RingHom.comp	—	comp_eval₂Hom
map_id 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map RingHom.id Semiring.toNonAssocSemiring	—	eval₂_eta
map_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	MvPolynomial DFunLike.coe RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map	—	coeff_map
map_injective_iff 📖	mathematical	—	MvPolynomial DFunLike.coe RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map Semiring.toNonAssocSemiring	—	map_C map_injective
map_leftInverse 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	MvPolynomial DFunLike.coe RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map	—	map_map RingHom.ext map_id
map_map 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map RingHom.comp Semiring.toNonAssocSemiring	—	eval₂_comp_left RingHom.ext map_C map_X
map_mapRange_eq_iff 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map Finsupp.mapRange NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring coeff	—	coeff_map
map_monomial 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike monomial	—	eval₂_monomial monomial_eq
map_ofNat 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map	—	map_ofNat RingHom.instRingHomClass
map_rightInverse 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	MvPolynomial DFunLike.coe RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map	—	Function.LeftInverse.rightInverse map_leftInverse Function.RightInverse.leftInverse
map_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	MvPolynomial DFunLike.coe RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map	—	induction_on' map_monomial map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
map_surjective_iff 📖	mathematical	—	MvPolynomial DFunLike.coe RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map Semiring.toNonAssocSemiring	—	coeff_map coeff_zero_C map_surjective
mem_range_map_iff_coeffs_subset 📖	mathematical	—	MvPolynomial Set Set.instMembership Set.range DFunLike.coe RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map Set.instHasSubset SetLike.coe Finset Finset.instSetLike coeffs Semiring.toNonAssocSemiring	—	subset_trans Set.instIsTransSubset coe_coeffs_map Set.preimage_range induction_on'' map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass C_0 coeffs_C Finset.coe_singleton map_C Finset.coe_union coeffs_add disjoint_support_monomial map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass coeffs_mul_X map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_X
range_mapAlgHom 📖	mathematical	—	DFunLike.coe OrderEmbedding Subalgebra MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule AlgHom.range mapAlgHom coeffsIn	—	Submodule.ext Subalgebra.mem_toSubmodule SetLike.mem_coe AlgHom.coe_range mapAlgHom.eq_1 mem_range_map_iff_coeffs_subset mem_coeffsIn_iff_coeffs_subset
smul_eval 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval Algebra.toSMul AddMonoidAlgebra.semiring Finsupp.instAddMonoid AddMonoidAlgebra.algebra Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	smul_eq_C_mul RingHom.map_mul eval_C
support_map_of_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	support DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map	—	Finset.Subset.antisymm support_map_subset Mathlib.Tactic.Contrapose.contrapose₄ RingHom.map_zero coeff_map
support_map_subset 📖	mathematical	—	Finset Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset.instHasSubset support DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike map	—	Mathlib.Tactic.Contrapose.contrapose₄ coeff_map map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass

---

← Back to Index