Bivariate

📁 Source: Mathlib/Algebra/Polynomial/Bivariate.lean

Statistics

Metric	Count
Definitions evalEval, equivMvPolynomial, swap, termY, «term_[X][Y]», CC, aevalAeval, evalEval, evalEvalRingHom	9
Theorems evalEval_apply, evalEval_mk, pderiv_one_equivMvPolynomial, pderiv_zero_equivMvPolynomial, aevalAeval_swap, aveal_eq_map_swap, equivMvPolynomial_C_C, equivMvPolynomial_C_X, equivMvPolynomial_X, equivMvPolynomial_symm_C, equivMvPolynomial_symm_X_0, equivMvPolynomial_symm_X_1, pderiv_one_equivMvPolynomial, pderiv_zero_equivMvPolynomial, swap_C, swap_C_C, swap_X, swap_Y, swap_apply, swap_map_C, swap_monomial_monomial, coe_aevalAeval_eq_evalEval, coe_algebraMap_eq_CC, coe_evalEvalRingHom, evalEvalRingHom_apply, evalEvalRingHom_eq, evalEval_C, evalEval_CC, evalEval_X, evalEval_add, evalEval_dvd, evalEval_finset_sum, evalEval_intCast, evalEval_list_prod, evalEval_map_C, evalEval_mul, evalEval_multiset_prod, evalEval_natCast, evalEval_neg, evalEval_one, evalEval_pow, evalEval_prod, evalEval_smul, evalEval_sub, evalEval_sum, evalEval_surjective, evalEval_zero, eval_C_X_comp_eval₂_map_C_X, eval_C_X_eval₂_map_C_X, eval₂RingHom_eval₂RingHom, eval₂_evalRingHom, eval₂_eval₂RingHom_apply, map_evalRingHom_eval, map_mapRingHom_evalEval, map_mapRingHom_eval_map, map_mapRingHom_eval_map_eval	56
Total	65

AdjoinRoot

Definitions

Name	Category	Theorems
evalEval 📖	CompOp	2 math math: evalEval_apply, evalEval_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
evalEval_apply 📖	mathematical	Polynomial.evalEval CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DFunLike.coe RingHom AdjoinRoot Polynomial Polynomial.commRing Semiring.toNonAssocSemiring instCommRing RingHom.instFunLike evalEval AddMonoidHom HasQuotient.Quotient AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup Polynomial.ring CommRing.toRing QuotientAddGroup.instHasQuotientAddSubgroup Submodule.toAddSubgroup Semiring.toModule Ring.toSemiring Ideal.span Polynomial.semiring Set Set.instSingletonSet AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddMonoidHom.instFunLike QuotientAddGroup.lift AddMonoidHomClass.toAddMonoidHom RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Polynomial.eval₂RingHom Polynomial.evalRingHom	—	—
evalEval_mk 📖	mathematical	Polynomial.evalEval CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DFunLike.coe RingHom AdjoinRoot Polynomial Polynomial.commRing Semiring.toNonAssocSemiring instCommRing RingHom.instFunLike evalEval Polynomial.semiring	—	evalEval.eq_1 Polynomial.eval₂_evalRingHom

Polynomial

Definitions

Name	Category	Theorems
CC 📖	CompOp	2 math math: evalEval_CC, coe_algebraMap_eq_CC
aevalAeval 📖	CompOp	3 math math: Bivariate.swap_apply, Bivariate.aevalAeval_swap, coe_aevalAeval_eq_evalEval
evalEval 📖	CompOp	41 math math: evalEval_finset_sum, evalEval_intCast, WeierstrassCurve.Jacobian.eval_polynomialX_of_Z_ne_zero, evalEval_dvd, evalEval_sum, WeierstrassCurve.Jacobian.eval_polynomialY_of_Z_ne_zero, evalEval_X, evalEval_multiset_prod, evalEval_CC, evalEval_prod, WeierstrassCurve.Projective.eval_polynomialX_of_Z_ne_zero, evalEval_sub, map_mapRingHom_evalEval, WeierstrassCurve.Affine.evalEval_polynomial_zero, evalEval_pow, WeierstrassCurve.Projective.eval_polynomialY_of_Z_ne_zero, eval₂_evalRingHom, WeierstrassCurve.Affine.evalEval_polynomialY_zero, evalEval_add, WeierstrassCurve.Affine.slope_of_Y_ne_eq_evalEval, evalEval_neg, WeierstrassCurve.Affine.evalEval_polynomialY, WeierstrassCurve.Projective.eval_polynomial_of_Z_ne_zero, WeierstrassCurve.Jacobian.eval_polynomial_of_Z_ne_zero, WeierstrassCurve.Affine.evalEval_polynomial, evalEval_zero, WeierstrassCurve.Affine.evalEval_polynomialX, evalEval_map_C, evalEval_list_prod, evalEval_smul, evalEval_surjective, coe_aevalAeval_eq_evalEval, evalEval_natCast, evalEval_C, WeierstrassCurve.Affine.evalEval_negPolynomial, map_evalRingHom_eval, WeierstrassCurve.Affine.evalEval_polynomialX_zero, coe_evalEvalRingHom, eval₂_eval₂RingHom_apply, evalEval_one, evalEval_mul
evalEvalRingHom 📖	CompOp	4 math math: eval₂RingHom_eval₂RingHom, evalEvalRingHom_eq, evalEvalRingHom_apply, coe_evalEvalRingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_aevalAeval_eq_evalEval 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike aevalAeval evalEval	—	Algebra.commutes mapRingHom_id AlgHom.restrictScalars.congr_simp eval₂AlgHom'.congr_simp
coe_algebraMap_eq_CC 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring semiring Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap algebraOfAlgebra Algebra.id CC	—	—
coe_evalEvalRingHom 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring semiring Semiring.toNonAssocSemiring RingHom.instFunLike evalEvalRingHom evalEval	—	—
evalEvalRingHom_apply 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring semiring Semiring.toNonAssocSemiring RingHom.instFunLike evalEvalRingHom eval commSemiring C	—	—
evalEvalRingHom_eq 📖	mathematical	—	evalEvalRingHom eval₂RingHom Polynomial CommSemiring.toSemiring semiring evalRingHom	—	ringHom_ext' RingHom.ext eval_C eval₂_C eval_X eval₂_X
evalEval_C 📖	mathematical	—	evalEval DFunLike.coe RingHom Polynomial semiring Semiring.toNonAssocSemiring RingHom.instFunLike C eval	—	evalEval.eq_1 eval_C
evalEval_CC 📖	mathematical	—	evalEval CC	—	evalEval_C eval_C
evalEval_X 📖	mathematical	—	evalEval X Polynomial semiring	—	evalEval.eq_1 eval_X eval_C
evalEval_add 📖	mathematical	—	evalEval Polynomial semiring instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	eval_add
evalEval_dvd 📖	mathematical	Polynomial CommSemiring.toSemiring semiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring commSemiring	evalEval	—	eval_dvd
evalEval_finset_sum 📖	mathematical	—	evalEval Finset.sum Polynomial semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	eval_finset_sum Finset.sum_congr
evalEval_intCast 📖	mathematical	—	evalEval Ring.toSemiring Polynomial semiring instIntCast ring AddGroupWithOne.toIntCast Ring.toAddGroupWithOne	—	eval_intCast
evalEval_list_prod 📖	mathematical	—	evalEval CommSemiring.toSemiring Polynomial semiring instMul instOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	eval_list_prod
evalEval_map_C 📖	mathematical	—	evalEval map Polynomial semiring C eval	—	evalEval.eq_1 eval_map_apply eval_C
evalEval_mul 📖	mathematical	—	evalEval CommSemiring.toSemiring Polynomial semiring instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	eval_mul
evalEval_multiset_prod 📖	mathematical	—	evalEval CommSemiring.toSemiring Multiset.prod Polynomial semiring CommSemiring.toCommMonoid commSemiring Multiset.map	—	eval_multiset_prod Multiset.map_map Multiset.map_congr
evalEval_natCast 📖	mathematical	—	evalEval Polynomial semiring instNatCast AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	eval_natCast
evalEval_neg 📖	mathematical	—	evalEval Ring.toSemiring Polynomial semiring instNeg ring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	eval_neg
evalEval_one 📖	mathematical	—	evalEval Polynomial semiring instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	eval_one
evalEval_pow 📖	mathematical	—	evalEval CommSemiring.toSemiring Polynomial semiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	eval_pow
evalEval_prod 📖	mathematical	—	evalEval CommSemiring.toSemiring Finset.prod Polynomial semiring CommSemiring.toCommMonoid commSemiring	—	eval_prod Finset.prod_congr
evalEval_smul 📖	mathematical	—	evalEval Polynomial semiring SMulZeroClass.toSMul instZero smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring AddZero.toZero AddZeroClass.toAddZero	—	eval_smul isScalarTower_right
evalEval_sub 📖	mathematical	—	evalEval Ring.toSemiring Polynomial semiring instSub ring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	eval_sub
evalEval_sum 📖	mathematical	—	evalEval sum Polynomial semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	eval₂_sum
evalEval_surjective 📖	mathematical	—	Polynomial semiring evalEval	—	evalEval_CC
evalEval_zero 📖	mathematical	—	evalEval Polynomial semiring instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	eval_zero
eval_C_X_comp_eval₂_map_C_X 📖	mathematical	—	RingHom.comp Polynomial CommSemiring.toSemiring semiring commSemiring Semiring.toNonAssocSemiring evalRingHom DFunLike.coe RingHom RingHom.instFunLike C X eval₂RingHom mapRingHom algebraMap algebraOfAlgebra Algebra.id RingHom.id	—	ringHom_ext' RingHom.ext ext eval₂_C map_C eval_C RingHomCompTriple.comp_eq RingHomCompTriple.right_ids map_X eval_X eval₂_X
eval_C_X_eval₂_map_C_X 📖	mathematical	—	eval Polynomial CommSemiring.toSemiring semiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C X eval₂ mapRingHom algebraMap algebraOfAlgebra Algebra.id	—	eval_C_X_comp_eval₂_map_C_X
eval₂RingHom_eval₂RingHom 📖	mathematical	—	eval₂RingHom Polynomial CommSemiring.toSemiring semiring RingHom.comp Semiring.toNonAssocSemiring evalEvalRingHom mapRingHom	—	ringHom_ext' RingHom.ext eval₂_C map_C eval_C eval₂_X map_X eval_X
eval₂_evalRingHom 📖	mathematical	—	eval₂ Polynomial CommSemiring.toSemiring semiring evalRingHom evalEval	—	coe_evalEvalRingHom evalEvalRingHom_eq coe_eval₂RingHom
eval₂_eval₂RingHom_apply 📖	mathematical	—	eval₂ Polynomial CommSemiring.toSemiring semiring eval₂RingHom evalEval map mapRingHom	—	eval₂RingHom_eval₂RingHom
map_evalRingHom_eval 📖	mathematical	—	eval CommSemiring.toSemiring map Polynomial semiring evalRingHom evalEval	—	eval_map eval₂_evalRingHom
map_mapRingHom_evalEval 📖	mathematical	—	evalEval DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike map Polynomial semiring mapRingHom	—	evalEval.eq_1 map_mapRingHom_eval_map_eval map_C
map_mapRingHom_eval_map 📖	mathematical	—	eval Polynomial semiring map mapRingHom	—	eval_map coe_mapRingHom eval₂_hom
map_mapRingHom_eval_map_eval 📖	mathematical	—	eval DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial semiring map mapRingHom	—	map_mapRingHom_eval_map eval_map eval₂_hom

Polynomial.Bivariate

Definitions

Name	Category	Theorems
equivMvPolynomial 📖	CompOp	17 math math: StandardEtalePresentation.toPresentation_algebra_smul, Polynomial.Bivariate.pderiv_one_equivMvPolynomial, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, equivMvPolynomial_symm_X_0, equivMvPolynomial_symm_C, equivMvPolynomial_symm_X_1, pderiv_zero_equivMvPolynomial, equivMvPolynomial_X, equivMvPolynomial_C_X, Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, StandardEtalePresentation.toPresentation_σ', StandardEtalePresentation.aeval_val_equivMvPolynomial, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, StandardEtalePresentation.toPresentation_val, StandardEtalePresentation.toPresentation_relation, pderiv_one_equivMvPolynomial, equivMvPolynomial_C_C
swap 📖	CompOp	9 math math: aveal_eq_map_swap, swap_apply, swap_Y, swap_X, swap_C_C, swap_monomial_monomial, swap_map_C, aevalAeval_swap, swap_C
termY 📖	CompOp	—
«term_[X][Y]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aevalAeval_swap 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aevalAeval AlgEquiv AlgEquiv.instFunLike swap	—	Polynomial.induction_on' map_add SemilinearMapClass.toAddHomClass AlgHomClass.linearMapClass AlgHom.algHomClass Polynomial.eval_add NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass Polynomial.aeval_monomial Polynomial.eval_mul Polynomial.eval_map_algebraMap Polynomial.eval_pow Polynomial.eval_C map_mul NonUnitalAlgSemiHomClass.toMulHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass Polynomial.aeval_C Polynomial.map_X Polynomial.eval_X add_mul Distrib.rightDistribClass Polynomial.map_C Polynomial.aeval_X
aveal_eq_map_swap 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Polynomial.commSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id Polynomial.algebra AlgHom.funLike Polynomial.aeval RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Polynomial.mapAlgHom AlgEquiv AlgEquiv.instFunLike swap	—	Polynomial.induction_on' AlgHomClass.toRingHomClass AlgHom.algHomClass map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHomClass.linearMapClass Polynomial.eval_add Polynomial.map_add Polynomial.aeval_monomial Polynomial.eval_mul Polynomial.eval_map_algebraMap Polynomial.eval_pow Polynomial.eval_C Polynomial.map_mul Polynomial.map_pow Polynomial.map_C Polynomial.aeval_X add_mul Distrib.rightDistribClass Polynomial.map_monomial Polynomial.C_mul_X_pow_eq_monomial Polynomial.aeval_C
equivMvPolynomial_C_C 📖	mathematical	—	DFunLike.coe AlgEquiv Polynomial CommSemiring.toSemiring Polynomial.semiring MvPolynomial MvPolynomial.commSemiring Polynomial.algebraOfAlgebra Algebra.id MvPolynomial.algebra AlgEquiv.instFunLike equivMvPolynomial RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C MvPolynomial.C	—	Polynomial.aeval_C Polynomial.map_C Polynomial.eval_C
equivMvPolynomial_C_X 📖	mathematical	—	DFunLike.coe AlgEquiv Polynomial CommSemiring.toSemiring Polynomial.semiring MvPolynomial MvPolynomial.commSemiring Polynomial.algebraOfAlgebra Algebra.id MvPolynomial.algebra AlgEquiv.instFunLike equivMvPolynomial RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Polynomial.X MvPolynomial.X	—	Polynomial.aeval_C Polynomial.map_X Polynomial.eval_X
equivMvPolynomial_X 📖	mathematical	—	DFunLike.coe AlgEquiv Polynomial CommSemiring.toSemiring Polynomial.semiring MvPolynomial MvPolynomial.commSemiring Polynomial.algebraOfAlgebra Algebra.id MvPolynomial.algebra AlgEquiv.instFunLike equivMvPolynomial Polynomial.X MvPolynomial.X	—	Polynomial.aeval_X Polynomial.eval_C
equivMvPolynomial_symm_C 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial CommSemiring.toSemiring Polynomial.semiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike AlgEquiv.symm equivMvPolynomial RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.C Polynomial.C	—	MvPolynomial.algHom_C
equivMvPolynomial_symm_X_0 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial CommSemiring.toSemiring Polynomial.semiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike AlgEquiv.symm equivMvPolynomial MvPolynomial.X RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Polynomial.X	—	MvPolynomial.aeval_X
equivMvPolynomial_symm_X_1 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial CommSemiring.toSemiring Polynomial.semiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike AlgEquiv.symm equivMvPolynomial MvPolynomial.X Polynomial.X	—	MvPolynomial.aeval_X Matrix.cons_val_fin_one
pderiv_one_equivMvPolynomial 📖	mathematical	—	DFunLike.coe Derivation MvPolynomial MvPolynomial.commSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.algebra Algebra.id Semiring.toModule MvPolynomial.module Derivation.instFunLike MvPolynomial.pderiv AlgEquiv Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra AlgEquiv.instFunLike equivMvPolynomial LinearMap RingHom.id Polynomial.module LinearMap.instFunLike Polynomial.derivative	—	Polynomial.induction_on' map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AddMonoidHomClass.toAddHomClass Derivation.instAddMonoidHomClass Polynomial.derivative_add LinearMap.semilinearMapClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass NonUnitalAlgSemiHomClass.toMulHomClass equivMvPolynomial_C_C AlgHomClass.toRingHomClass equivMvPolynomial_C_X equivMvPolynomial_X Derivation.leibniz Derivation.leibniz_pow MvPolynomial.pderiv_X Pi.single_eq_same mul_one nsmul_eq_mul Pi.single_eq_of_ne Fin.instNeZeroHAddNatOfNat_mathlib_1 MulZeroClass.mul_zero nsmul_zero MvPolynomial.derivation_C add_zero Polynomial.derivative_mul Polynomial.derivative_C MulZeroClass.zero_mul Polynomial.derivative_pow map_natCast Polynomial.derivative_X zero_add
pderiv_zero_equivMvPolynomial 📖	mathematical	—	DFunLike.coe Derivation MvPolynomial CommRing.toCommSemiring MvPolynomial.commSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.algebra Algebra.id Semiring.toModule MvPolynomial.module Derivation.instFunLike MvPolynomial.pderiv AlgEquiv Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra AlgEquiv.instFunLike equivMvPolynomial LinearEquiv Polynomial.commRing RingHom.id RingHomInvPair.ids PolynomialModule Ring.toAddCommGroup CommRing.toRing AddCommGroup.toAddCommMonoid instAddCommGroupPolynomialModule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing PolynomialModule.polynomialModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv PolynomialModule.equivPolynomialSelf Polynomial.ring Polynomial.commSemiring PolynomialModule.instModule Polynomial.module Derivation.mapCoeffs Polynomial.derivative'	—	Polynomial.induction_on' RingHomInvPair.ids map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AddMonoidHomClass.toAddHomClass Derivation.instAddMonoidHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearMap.semilinearMapClass Derivation.mapCoeffs_monomial map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass NonUnitalAlgSemiHomClass.toMulHomClass equivMvPolynomial_C_C AlgHomClass.toRingHomClass equivMvPolynomial_C_X equivMvPolynomial_X Derivation.leibniz Derivation.leibniz_pow MvPolynomial.pderiv_X Pi.single_eq_of_ne Fin.instNeZeroHAddNatOfNat_mathlib_1 MulZeroClass.mul_zero nsmul_zero Pi.single_eq_same mul_one nsmul_eq_mul MvPolynomial.derivation_C add_zero zero_add Derivation.mapCoeffs_X smul_zero Derivation.mapCoeffs_C Polynomial.derivative_X Polynomial.derivation_C map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass map_smul SemilinearMapClass.toMulActionSemiHomClass map_nsmul DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass map_one MonoidHomClass.toOneHomClass map_natCast
swap_C 📖	mathematical	—	DFunLike.coe AlgEquiv Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgEquiv.instFunLike swap RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Polynomial.map	—	AlgHom.restrictScalars.congr_simp RingHomCompTriple.comp_apply RingHomCompTriple.right_ids Polynomial.aeval_C Polynomial.eval_map_algebraMap Polynomial.aeval_X_left_eq_map
swap_C_C 📖	mathematical	—	DFunLike.coe AlgEquiv Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgEquiv.instFunLike swap RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	—	Polynomial.aeval_C Polynomial.map_C Polynomial.eval_C
swap_X 📖	mathematical	—	DFunLike.coe AlgEquiv Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgEquiv.instFunLike swap RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Polynomial.X	—	Polynomial.aeval_C Polynomial.map_X Polynomial.eval_X
swap_Y 📖	mathematical	—	DFunLike.coe AlgEquiv Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgEquiv.instFunLike swap Polynomial.X RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	—	Polynomial.aeval_X Polynomial.eval_C
swap_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgEquiv.instFunLike swap AlgHom Polynomial.commSemiring AlgHom.funLike Polynomial.aevalAeval Polynomial.X RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	—	—
swap_map_C 📖	mathematical	—	DFunLike.coe AlgEquiv Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgEquiv.instFunLike swap Polynomial.map Polynomial.C RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	Polynomial.induction_on' Polynomial.map_add map_add SemilinearMapClass.toAddHomClass AlgHomClass.linearMapClass AlgHom.algHomClass Polynomial.eval_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Polynomial.map_monomial Polynomial.C_mul_X_pow_eq_monomial map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass swap_Y Polynomial.C_mul Polynomial.C_pow swap_C_C
swap_monomial_monomial 📖	mathematical	—	DFunLike.coe AlgEquiv Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgEquiv.instFunLike swap LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Polynomial.module LinearMap.instFunLike Polynomial.monomial	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Polynomial.aeval_C Polynomial.map_C AlgHomClass.toRingHomClass Polynomial.map_X Polynomial.aeval_X Polynomial.eval_mul Polynomial.eval_C Polynomial.eval_pow Polynomial.eval_X Semigroup.to_isAssociative CommMagma.to_isCommutative

Polynomial.Bivariate.Polynomial.Bivariate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pderiv_one_equivMvPolynomial 📖	mathematical	—	DFunLike.coe Derivation MvPolynomial MvPolynomial.commSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.algebra Algebra.id Semiring.toModule MvPolynomial.module Derivation.instFunLike MvPolynomial.pderiv AlgEquiv Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra AlgEquiv.instFunLike Polynomial.Bivariate.equivMvPolynomial LinearMap RingHom.id Polynomial.module LinearMap.instFunLike Polynomial.derivative	—	Polynomial.Bivariate.pderiv_one_equivMvPolynomial
pderiv_zero_equivMvPolynomial 📖	mathematical	—	DFunLike.coe Derivation MvPolynomial CommRing.toCommSemiring MvPolynomial.commSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.algebra Algebra.id Semiring.toModule MvPolynomial.module Derivation.instFunLike MvPolynomial.pderiv AlgEquiv Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra AlgEquiv.instFunLike Polynomial.Bivariate.equivMvPolynomial LinearEquiv Polynomial.commRing RingHom.id RingHomInvPair.ids PolynomialModule Ring.toAddCommGroup CommRing.toRing AddCommGroup.toAddCommMonoid instAddCommGroupPolynomialModule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing PolynomialModule.polynomialModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv PolynomialModule.equivPolynomialSelf Polynomial.ring Polynomial.commSemiring PolynomialModule.instModule Polynomial.module Derivation.mapCoeffs Polynomial.derivative'	—	Polynomial.Bivariate.pderiv_zero_equivMvPolynomial

---

← Back to Index