Eval

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

Statistics

Metric	Count
Definitions aeval, aevalTower, algebraMvPolynomial, eval, eval₂, eval₂Hom, map, mapAlgHom	8
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_sum, aeval_sumElim, aeval_unique, aeval_zero, aeval_zero', algebraMap_def, coe_aeval_eq_eval, coe_coeffs_map, 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₂Hom_C, eval₂Hom_X', eval₂Hom_congr, eval₂Hom_eq_zero, eval₂Hom_map_hom, eval₂Hom_monomial, eval₂Hom_zero, eval₂Hom_zero', eval₂Hom_zero'_apply, eval₂Hom_zero_apply, eval₂_C, eval₂_X, 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_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	124
Total	132

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_eq_range 📖	mathematical	—	adjoin CommSemiring.toSemiring AlgHom.range MvPolynomial Set Set.instMembership MvPolynomial.commSemiring MvPolynomial.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 MvPolynomial.commSemiring MvPolynomial.algebra id MvPolynomial.aeval	—	AlgHom.map_adjoin MvPolynomial.aeval_X

MvPolynomial

Definitions

Name	Category	Theorems
aeval 📖	CompOp	140 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_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, 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	95 math math: funext_iff, eval_indicator_apply_eq_one, Ideal.mem_span_iff_exists_isHomogeneous, eval_zero', WeierstrassCurve.Projective.eval_polynomial, isEmptyRingEquiv_apply, WeierstrassCurve.Projective.polynomial_relation, AnalyticOnNhd.eval_linearMap', WeierstrassCurve.Jacobian.eval_polynomialY, eval_map, char_dvd_card_solutions_of_add_lt, aeval_eq_eval, schwartz_zippel_totalDegree, eval_mem, eval_rename_prod_mk, eval_eval₂, eval₂_id, 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, 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, WeierstrassCurve.Projective.eval_polynomialZ, eval_pow, 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, WeierstrassCurve.Projective.negDblY_eq', LinearMap.polyCharpolyAux_coeff_eval, eval_sub, 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, WeierstrassCurve.Projective.dblX_eq, coeff_eval_eq_eval_coeff, optionEquivLeft_elim_eval, 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	62 math math: 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₂_C, rename_eval₂, eval₂_cast_comp, eval₂_dvd, 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, eval₂_map_comp_C, rename_prod_mk_eval₂, eval₂_mul_C, 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₂Hom 📖	CompOp	44 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, hom_bind₁, eval₂Hom_comp_expand, eval₂Hom_comp_C
map 📖	CompOp	107 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, 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 commSemiring C map	—	C_dvd_iff_dvd_coeff ext_iff coeff_map
aevalTower_C 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra AlgHom.funLike aevalTower RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	eval₂_C
aevalTower_X 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra AlgHom.funLike aevalTower X	—	eval₂_X
aevalTower_algebraMap 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring 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 commSemiring RingHomClass.toRingHom AlgHom 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 commSemiring RingHomClass.toRingHom AlgHom algebra AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass aevalTower algebraMap Algebra.id	—	aevalTower_comp_C
aevalTower_comp_toAlgHom 📖	mathematical	—	AlgHom.comp MvPolynomial CommSemiring.toSemiring commSemiring algebra aevalTower 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	—	AlgHom.coe_ringHom_injective 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 CommSemiring.toSemiring commSemiring algebra AlgHom.funLike aevalTower	—	map_ofNat AlgHomClass.toRingHomClass AlgHom.algHomClass
aevalTower_toAlgHom 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra AlgHom.funLike aevalTower 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	—	aevalTower_algebraMap
aeval_C 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C algebraMap	—	eval₂_C
aeval_X 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval X	—	eval₂_X
aeval_X_left 📖	mathematical	—	aeval MvPolynomial commSemiring algebra Algebra.id X AlgHom.id CommSemiring.toSemiring	—	aeval_unique
aeval_X_left_apply 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval X	—	AlgHom.congr_fun aeval_X_left
aeval_def 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval eval₂ algebraMap	—	—
aeval_eq_eval 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval RingHom Semiring.toNonAssocSemiring RingHom.instFunLike eval	—	—
aeval_eq_eval₂Hom 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval RingHom Semiring.toNonAssocSemiring RingHom.instFunLike eval₂Hom algebraMap	—	—
aeval_eq_zero 📖	mathematical	Finset Finset.instMembership Finsupp.support MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	DFunLike.coe AlgHom MvPolynomial commSemiring algebra Algebra.id AlgHom.funLike aeval	—	eval₂Hom_eq_zero
aeval_monomial 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike algebraMap Finsupp.prod MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toCommMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	eval₂Hom_monomial
aeval_ofNat 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval	—	map_ofNat AlgHomClass.toRingHomClass AlgHom.algHomClass
aeval_prod 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval Finset.prod CommSemiring.toCommMonoid	—	map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
aeval_sum 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass
aeval_sumElim 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap X 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 CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike X	—	algHom_ext aeval_X
aeval_zero 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring RingHom RingHom.instFunLike algebraMap constantCoeff	—	eval₂Hom_zero_apply
aeval_zero' 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring RingHom RingHom.instFunLike algebraMap constantCoeff	—	aeval_zero
algebraMap_def 📖	mathematical	—	algebraMap MvPolynomial commSemiring CommSemiring.toSemiring algebraMvPolynomial map	—	—
coe_aeval_eq_eval 📖	mathematical	—	RingHomClass.toRingHom AlgHom MvPolynomial CommSemiring.toSemiring commSemiring 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map Set.image	—	instIsConcreteLE coeffs_map
coe_eval₂Hom 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval₂Hom eval₂	—	—
coeff_map 📖	mathematical	—	coeff DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map	—	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 Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map Finset.image	—	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 CommSemiring.toSemiring commSemiring 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 commSemiring algebra Algebra.id aeval	—	comp_aeval AlgHom.coe_comp
comp_eval₂Hom 📖	mathematical	—	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike constantCoeff map	—	coeff_map
eval_C 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval C	—	eval₂_C
eval_X 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval X	—	eval₂_X
eval_add 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	eval₂_add
eval_assoc 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval eval₂ C	—	eval₂_comp_left RingHom.ext eval₂_C
eval_eq 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval Finset.sum Finsupp MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring support Distrib.toMul NonUnitalNonAssocSemiring.toDistrib coeff Finset.prod CommSemiring.toCommMonoid Finsupp.support Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Finsupp.instFunLike	—	—
eval_eq' 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval Finset.sum Finsupp MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring support Distrib.toMul NonUnitalNonAssocSemiring.toDistrib coeff Finset.prod CommSemiring.toCommMonoid Finset.univ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Finsupp.instFunLike	—	eval₂_eq'
eval_eval₂ 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval eval₂ 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring 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	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval	—	eval₂_mem
eval_monomial 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Finsupp.prod MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toCommMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	eval₂_monomial
eval_mul 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	eval₂_mul
eval_ofNat 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval	—	map_ofNat RingHom.instRingHomClass
eval_pow 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	eval₂_pow
eval_prod 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval Finset.prod CommSemiring.toCommMonoid	—	map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
eval_sum 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval Finset.sum 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₂Hom_C 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval₂Hom C	—	eval₂_C
eval₂Hom_X' 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval₂Hom X	—	eval₂_X
eval₂Hom_congr 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval₂Hom	—	—
eval₂Hom_eq_zero 📖	mathematical	Finset Finset.instMembership Finsupp.support MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	DFunLike.coe RingHom MvPolynomial commSemiring RingHom.instFunLike eval₂Hom	—	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 Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval₂Hom map RingHom.comp	—	eval₂_map
eval₂Hom_monomial 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval₂Hom LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Finsupp.prod MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toCommMonoid Monoid.toNatPow 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_zero 📖	mathematical	—	eval₂Hom Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.comp MvPolynomial commSemiring 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 commSemiring constantCoeff	—	eval₂Hom_zero
eval₂Hom_zero'_apply 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval₂Hom MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring constantCoeff	—	eval₂Hom_zero_apply
eval₂Hom_zero_apply 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval₂Hom Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring constantCoeff	—	RingHom.congr_fun eval₂Hom_zero
eval₂_C 📖	mathematical	—	eval₂ DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring 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₂_add 📖	mathematical	—	eval₂ MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring	—	Finsupp.sum_add_index RingHom.map_zero MulZeroClass.zero_mul RingHom.map_add add_mul Distrib.rightDistribClass
eval₂_assoc 📖	mathematical	—	eval₂ MvPolynomial commSemiring C	—	eval₂_comp_left RingHom.ext eval₂_C
eval₂_comp 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike MvPolynomial commSemiring 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 commSemiring 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 NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring commSemiring	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.toNatPow 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.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Finsupp.instFunLike	—	Finset.sum_congr
eval₂_eq_eval_map 📖	mathematical	—	eval₂ DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval map	—	eval₂_comp_left RingHom.ext eval₂_C eval₂_X
eval₂_eta 📖	mathematical	—	eval₂ MvPolynomial commSemiring 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 commSemiring RingHom.instFunLike eval	—	—
eval₂_map 📖	mathematical	—	eval₂ DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map RingHom.comp	—	eval_map map_map
eval₂_map_comp_C 📖	mathematical	—	eval₂ MvPolynomial commSemiring RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring 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	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 commSemiring Semiring.toModule module LinearMap.instFunLike monomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike Finsupp.prod MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toCommMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Finsupp.sum_single_index RingHom.map_zero MulZeroClass.zero_mul
eval₂_mul 📖	mathematical	—	eval₂ MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring	—	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 Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring DFunLike.coe RingHom RingHom.instFunLike C	—	eval₂_mul_monomial mul_one
eval₂_mul_monomial 📖	mathematical	—	eval₂ 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 RingHom RingHom.instFunLike Finsupp.prod MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toCommMonoid Monoid.toNatPow 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring	—	eval₂_C map_natCast RingHom.instRingHomClass
eval₂_ofNat 📖	mathematical	—	eval₂	—	eval₂_natCast
eval₂_one 📖	mathematical	—	eval₂ MvPolynomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring	—	eval₂_C RingHom.map_one
eval₂_pow 📖	mathematical	—	eval₂ MvPolynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring	—	pow_zero eval₂_one pow_add pow_one eval₂_mul
eval₂_prod 📖	mathematical	—	eval₂ Finset.prod MvPolynomial CommSemiring.toCommMonoid commSemiring	—	map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
eval₂_sum 📖	mathematical	—	eval₂ Finset.sum MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring	—	map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
eval₂_zero 📖	mathematical	—	eval₂ MvPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring	—	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 commSemiring 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 commSemiring constantCoeff	—	eval₂Hom_zero_apply
instFaithfulSMul 📖	mathematical	—	FaithfulSMul MvPolynomial Algebra.toSMul commSemiring CommSemiring.toSemiring algebraMvPolynomial	—	faithfulSMul_iff_algebraMap_injective map_injective FaithfulSMul.algebraMap_injective
instIsScalarTower 📖	mathematical	—	IsScalarTower MvPolynomial Algebra.toSMul CommSemiring.toSemiring commSemiring algebra Algebra.id algebraMvPolynomial	—	IsScalarTower.of_algebraMap_eq' RingHom.ext ext map_C
mapAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra AlgHom.funLike mapAlgHom eval₂ RingHom.comp Semiring.toNonAssocSemiring C RingHomClass.toRingHom X	—	—
mapAlgHom_coe_ringHom 📖	mathematical	—	RingHomClass.toRingHom AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass mapAlgHom map	—	RingHom.mk_coe AlgHomClass.toRingHomClass AlgHom.algHomClass
mapAlgHom_id 📖	mathematical	—	mapAlgHom AlgHom.id CommSemiring.toSemiring MvPolynomial commSemiring algebra	—	AlgHom.ext map_id
map_C 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map C	—	map_monomial
map_X 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map X	—	eval₂_X
map_aeval 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike AlgHom MvPolynomial commSemiring algebra Algebra.id AlgHom.funLike aeval eval₂Hom RingHom.comp algebraMap	—	comp_eval₂Hom
map_eval 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike MvPolynomial commSemiring eval map	—	eval₂_eq_eval_map eval₂_id eval₂_comp_right map_id
map_eval₂ 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map eval₂ 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 commSemiring eval₂Hom RingHom.comp	—	comp_eval₂Hom
map_id 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map RingHom.id	—	eval₂_eta
map_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	MvPolynomial commSemiring map	—	coeff_map
map_injective_iff 📖	mathematical	—	MvPolynomial DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map	—	map_C map_injective
map_leftInverse 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	MvPolynomial commSemiring map	—	map_map RingHom.ext map_id
map_map 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map RingHom.comp	—	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 commSemiring RingHom.instFunLike map Finsupp.mapRange Finsupp Nat.instMulZeroClass coeff	—	coeff_map coeff_mapRange
map_monomial 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial	—	eval₂_monomial monomial_eq
map_ofNat 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map	—	map_ofNat RingHom.instRingHomClass
map_rightInverse 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	MvPolynomial commSemiring map	—	Function.LeftInverse.rightInverse map_leftInverse Function.RightInverse.leftInverse
map_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	MvPolynomial commSemiring map	—	induction_on' map_monomial map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
map_surjective_iff 📖	mathematical	—	MvPolynomial DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map	—	coeff_map coeff_zero_C map_surjective
mem_range_map_iff_coeffs_subset 📖	mathematical	—	MvPolynomial Set Set.instMembership Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map Set.instHasSubset SetLike.coe Finset Finset.instSetLike coeffs	—	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 CommSemiring.toSemiring commSemiring 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval Algebra.toSMul 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 MvPolynomial commSemiring 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike map	—	Mathlib.Tactic.Contrapose.contrapose₄ coeff_map map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass

---

← Back to Index