Equiv

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

Statistics

Metric	Count
Definitions commAlgEquiv, finSuccEquiv, isEmptyAlgEquiv, isEmptyRingEquiv, iterToSum, mapAlgEquiv, mapEquiv, mvPolynomialEquivMvPolynomial, optionEquivLeft, optionEquivRight, pUnitAlgEquiv, sumAlgEquiv, sumRingEquiv, sumToIter, toMvPolynomial	15
Theorems aeval_comp_toMvPolynomial, aeval_injective_iff_of_isEmpty, aeval_toMvPolynomial, coeff_eval_eq_eval_coeff, commAlgEquiv_C, commAlgEquiv_C_X, commAlgEquiv_X, degreeOf_coeff_finSuccEquiv, degreeOf_eq_natDegree, degree_finSuccEquiv, degree_optionEquivLeft, eval_comp_toMvPolynomial, eval_eq_eval_mv_eval', eval_toMvPolynomial, eval₂_const_pUnitAlgEquiv, eval₂_const_pUnitAlgEquiv_symm, eval₂_pUnitAlgEquiv, eval₂_pUnitAlgEquiv_symm, finSuccEquiv_X_succ, finSuccEquiv_X_zero, finSuccEquiv_apply, finSuccEquiv_coeff_coeff, finSuccEquiv_comp_C_eq_C, finSuccEquiv_eq, finSuccEquiv_rename_finSuccEquiv, image_support_finSuccEquiv, isEmptyAlgEquiv_apply, isEmptyRingEquiv_apply, isEmptyRingEquiv_eq_coeff_zero, isEmptyRingEquiv_symm_apply, isEmptyRingEquiv_symm_toRingHom, iterToSum_C_C, iterToSum_C_X, iterToSum_X, iterToSum_sumToIter, mapAlgEquiv_apply, mapAlgEquiv_refl, mapAlgEquiv_symm, mapAlgEquiv_trans, mapEquiv_apply, mapEquiv_refl, mapEquiv_symm, mapEquiv_trans, mem_image_support_coeff_finSuccEquiv, mem_support_coeff_finSuccEquiv, mem_support_coeff_optionEquivLeft, mem_support_finSuccEquiv, mvPolynomialEquivMvPolynomial_apply, mvPolynomialEquivMvPolynomial_symm_apply, natDegree_finSuccEquiv, natDegree_optionEquivLeft, nonempty_support_finSuccEquiv, nonempty_support_optionEquivLeft, optionEquivLeft_C, optionEquivLeft_X_none, optionEquivLeft_X_some, optionEquivLeft_apply, optionEquivLeft_coeff_coeff, optionEquivLeft_coeff_some_coeff_none, optionEquivLeft_elim_eval, optionEquivLeft_monomial, optionEquivLeft_symm_C_C, optionEquivLeft_symm_C_X, optionEquivLeft_symm_X, optionEquivLeft_symm_apply, optionEquivRight_C, optionEquivRight_X_none, optionEquivRight_X_some, optionEquivRight_apply, optionEquivRight_symm_apply, pUnitAlgEquiv_apply, pUnitAlgEquiv_monomial, pUnitAlgEquiv_symm_apply, pUnitAlgEquiv_symm_monomial, rename_comp_toMvPolynomial, rename_polynomial_aeval_X, rename_toMvPolynomial, sumAlgEquiv_apply, sumAlgEquiv_comp_rename_inl, sumAlgEquiv_comp_rename_inr, sumAlgEquiv_symm_apply, sumToIter_C, sumToIter_Xl, sumToIter_Xr, sumToIter_iterToSum, support_coeff_finSuccEquiv, support_finSuccEquiv, support_finSuccEquiv_nonempty, support_optionEquivLeft, totalDegree_coeff_finSuccEquiv_add_le, totalDegree_coeff_optionEquivLeft_add_le, totalDegree_coeff_optionEquivLeft_le, toMvPolynomial_C, toMvPolynomial_X, toMvPolynomial_eq_rename_comp, toMvPolynomial_injective	96
Total	111

MvPolynomial

Definitions

Name	Category	Theorems
commAlgEquiv 📖	CompOp	3 math math: commAlgEquiv_C, commAlgEquiv_X, commAlgEquiv_C_X
finSuccEquiv 📖	CompOp	22 math math: support_finSuccEquiv, mem_image_support_coeff_finSuccEquiv, natDegree_finSuccEquiv, totalDegree_coeff_finSuccEquiv_add_le, degreeOf_coeff_finSuccEquiv, nonempty_support_finSuccEquiv, support_finSuccEquiv_nonempty, eval_eq_eval_mv_eval', finSuccEquiv_coeff_coeff, support_coeff_finSuccEquiv, mem_support_finSuccEquiv, finSuccEquiv_comp_C_eq_C, finSuccEquiv_eq, image_support_finSuccEquiv, degree_finSuccEquiv, finSuccEquiv_X_succ, finSuccEquiv_apply, mem_support_coeff_finSuccEquiv, finSuccEquiv_rename_finSuccEquiv, finSuccEquiv_X_zero, IsHomogeneous.finSuccEquiv_coeff_isHomogeneous, eval_polynomial_eval_finSuccEquiv
isEmptyAlgEquiv 📖	CompOp	1 math math: isEmptyAlgEquiv_apply
isEmptyRingEquiv 📖	CompOp	4 math math: isEmptyRingEquiv_apply, isEmptyRingEquiv_symm_apply, isEmptyRingEquiv_symm_toRingHom, isEmptyRingEquiv_eq_coeff_zero
iterToSum 📖	CompOp	6 math math: iterToSum_sumToIter, iterToSum_C_X, iterToSum_X, sumToIter_iterToSum, sumAlgEquiv_symm_apply, iterToSum_C_C
mapAlgEquiv 📖	CompOp	4 math math: mapAlgEquiv_apply, mapAlgEquiv_refl, mapAlgEquiv_symm, mapAlgEquiv_trans
mapEquiv 📖	CompOp	4 math math: mapEquiv_symm, mapEquiv_apply, mapEquiv_trans, mapEquiv_refl
mvPolynomialEquivMvPolynomial 📖	CompOp	2 math math: mvPolynomialEquivMvPolynomial_symm_apply, mvPolynomialEquivMvPolynomial_apply
optionEquivLeft 📖	CompOp	22 math math: optionEquivLeft_C, optionEquivLeft_X_some, optionEquivLeft_apply, degree_optionEquivLeft, optionEquivLeft_X_none, optionEquivLeft_coeff_coeff, Matrix.charpoly.optionEquivLeft_symm_univ_isHomogeneous, mem_support_coeff_optionEquivLeft, totalDegree_coeff_optionEquivLeft_add_le, optionEquivLeft_coeff_some_coeff_none, natDegree_optionEquivLeft, nonempty_support_optionEquivLeft, support_optionEquivLeft, optionEquivLeft_monomial, optionEquivLeft_symm_apply, finSuccEquiv_rename_finSuccEquiv, optionEquivLeft_symm_C_X, degreeOf_eq_natDegree, optionEquivLeft_elim_eval, optionEquivLeft_symm_X, optionEquivLeft_symm_C_C, totalDegree_coeff_optionEquivLeft_le
optionEquivRight 📖	CompOp	5 math math: optionEquivRight_C, optionEquivRight_X_none, optionEquivRight_symm_apply, optionEquivRight_X_some, optionEquivRight_apply
pUnitAlgEquiv 📖	CompOp	11 math math: pUnitAlgEquiv_symm_monomial, pUnitAlgEquiv_apply, pUnitAlgEquiv_symm_apply, Polynomial.pUnitAlgEquiv_symm_toPowerSeries, eval₂_const_pUnitAlgEquiv_symm, Polynomial.toMvPolynomial_eq_rename_comp, eval₂_const_pUnitAlgEquiv, toMvPowerSeries_pUnitAlgEquiv, eval₂_pUnitAlgEquiv_symm, pUnitAlgEquiv_monomial, eval₂_pUnitAlgEquiv
sumAlgEquiv 📖	CompOp	4 math math: sumAlgEquiv_comp_rename_inr, sumAlgEquiv_comp_rename_inl, sumAlgEquiv_apply, sumAlgEquiv_symm_apply
sumRingEquiv 📖	CompOp	—
sumToIter 📖	CompOp	7 math math: iterToSum_sumToIter, pderiv_sumToIter, sumToIter_iterToSum, sumAlgEquiv_apply, sumToIter_Xr, sumToIter_C, sumToIter_Xl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_comp_toMvPolynomial 📖	mathematical	—	AlgHom.comp Polynomial CommSemiring.toSemiring MvPolynomial Polynomial.semiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.algebraOfAlgebra Algebra.id AddMonoidAlgebra.algebra aeval Polynomial.toMvPolynomial Polynomial.aeval	—	Polynomial.algHom_ext Polynomial.toMvPolynomial_X aeval_X Polynomial.aeval_X
aeval_injective_iff_of_isEmpty 📖	mathematical	—	MvPolynomial DFunLike.coe AlgHom 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	—	algHom_ext Function.Injective.of_comp_iff' AlgEquiv.bijective
aeval_toMvPolynomial 📖	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 Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Polynomial.toMvPolynomial Polynomial.aeval	—	DFunLike.congr_fun aeval_comp_toMvPolynomial
coeff_eval_eq_eval_coeff 📖	mathematical	—	Polynomial.coeff CommSemiring.toSemiring Polynomial.map MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid eval DFunLike.coe RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Semiring.toNonAssocSemiring RingHom.instFunLike	—	Polynomial.coeff_map
commAlgEquiv_C 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.semiring CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid AlgEquiv.instFunLike commAlgEquiv RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike C map	—	AddMonoidAlgebra.isScalarTower IsScalarTower.right algHom_ext iterToSum_C_X rename_X sumToIter_Xl eval₂_X DFunLike.congr_fun
commAlgEquiv_C_X 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.semiring CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid AlgEquiv.instFunLike commAlgEquiv RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike C X	—	commAlgEquiv_C map_X
commAlgEquiv_X 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.semiring CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid AlgEquiv.instFunLike commAlgEquiv X RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike C	—	iterToSum_X rename_X sumToIter_Xr
degreeOf_coeff_finSuccEquiv 📖	mathematical	—	degreeOf Polynomial.coeff MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv	—	degreeOf_eq_sup Finset.sup_le_iff Finsupp.cons_succ Finset.le_sup mem_support_coeff_finSuccEquiv
degreeOf_eq_natDegree 📖	mathematical	—	degreeOf Polynomial.natDegree MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft AlgHom AlgHom.funLike rename Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Equiv.optionSubtypeNe	—	natDegree_optionEquivLeft Equiv.optionSubtypeNe_symm_apply degreeOf_rename_of_injective Equiv.injective
degree_finSuccEquiv 📖	mathematical	—	Polynomial.degree MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv WithBot WithBot.natCast degreeOf	—	degreeOf_eq_sup support_finSuccEquiv Finset.sup_image Polynomial.degree.eq_1 Nat.cast_withBot Finset.coe_sup_of_nonempty nonempty_support_finSuccEquiv Finset.max_eq_sup_coe
degree_optionEquivLeft 📖	mathematical	—	Polynomial.degree MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft WithBot WithBot.natCast degreeOf	—	degreeOf_eq_sup support_optionEquivLeft Finset.sup_image Polynomial.degree.eq_1 Nat.cast_withBot Finset.coe_sup_of_nonempty nonempty_support_optionEquivLeft Finset.max_eq_sup_coe
eval_comp_toMvPolynomial 📖	mathematical	—	RingHom.comp Polynomial CommSemiring.toSemiring MvPolynomial Semiring.toNonAssocSemiring Polynomial.semiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid eval RingHomClass.toRingHom AlgHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid Polynomial.algebraOfAlgebra Algebra.id AddMonoidAlgebra.algebra AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass Polynomial.toMvPolynomial Polynomial.evalRingHom	—	Polynomial.ringHom_ext' AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.ext Polynomial.toMvPolynomial_C eval_C Polynomial.eval_C Polynomial.toMvPolynomial_X eval_X Polynomial.eval_X
eval_eq_eval_mv_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 Fin.cons Polynomial.eval Polynomial.map AddMonoidAlgebra.semiring Finsupp.instAddMonoid AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv	—	eval_C Polynomial.map_C algHom_ext Fin.forall_iff_succ aeval_X Fin.cons_zero finSuccEquiv_apply eval₂Hom_X' Polynomial.map_X Polynomial.eval_X Fin.cons_succ eval_X Polynomial.eval_C
eval_toMvPolynomial 📖	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 AlgHom Polynomial Polynomial.semiring AddMonoidAlgebra.semiring Finsupp.instAddMonoid Polynomial.algebraOfAlgebra Algebra.id AddMonoidAlgebra.algebra AlgHom.funLike Polynomial.toMvPolynomial Polynomial.eval	—	DFunLike.congr_fun AlgHomClass.toRingHomClass AlgHom.algHomClass eval_comp_toMvPolynomial
eval₂_const_pUnitAlgEquiv 📖	mathematical	—	Polynomial.eval₂ CommSemiring.toSemiring DFunLike.coe AlgEquiv MvPolynomial Polynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike pUnitAlgEquiv eval₂	—	eval₂_pUnitAlgEquiv
eval₂_const_pUnitAlgEquiv_symm 📖	mathematical	—	eval₂ DFunLike.coe AlgEquiv Polynomial CommSemiring.toSemiring MvPolynomial Polynomial.semiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.algebraOfAlgebra Algebra.id AddMonoidAlgebra.algebra AlgEquiv.instFunLike AlgEquiv.symm pUnitAlgEquiv Polynomial.eval₂	—	eval₂_pUnitAlgEquiv_symm
eval₂_pUnitAlgEquiv 📖	mathematical	—	Polynomial.eval₂ CommSemiring.toSemiring DFunLike.coe AlgEquiv MvPolynomial Polynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike pUnitAlgEquiv eval₂	—	induction_on' eval₂_monomial Finsupp.prod_pow Finset.prod_congr Finset.univ_unique Finset.prod_singleton Polynomial.eval₂_mul Polynomial.eval₂_C Polynomial.eval₂_X_pow eval₂_add Polynomial.eval₂_add
eval₂_pUnitAlgEquiv_symm 📖	mathematical	—	eval₂ DFunLike.coe AlgEquiv Polynomial CommSemiring.toSemiring MvPolynomial Polynomial.semiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.algebraOfAlgebra Algebra.id AddMonoidAlgebra.algebra AlgEquiv.instFunLike AlgEquiv.symm pUnitAlgEquiv Polynomial.eval₂	—	Polynomial.induction_on' Polynomial.eval₂_add eval₂_add Polynomial.eval₂_monomial eval₂_mul eval₂_C eval₂_pow eval₂_X
finSuccEquiv_X_succ 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv X RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	—	finSuccEquiv_apply eval₂Hom_X'
finSuccEquiv_X_zero 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv X Polynomial.X	—	finSuccEquiv_apply eval₂Hom_X'
finSuccEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Semiring.toNonAssocSemiring Polynomial.commSemiring AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid RingHom.instFunLike eval₂Hom RingHom.comp Polynomial.C C Polynomial.X X	—	AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass finSuccEquiv_eq RingHom.coe_coe
finSuccEquiv_coeff_coeff 📖	mathematical	—	coeff Polynomial.coeff MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv Finsupp.cons	—	induction_on' finSuccEquiv_apply eval₂_monomial Finsupp.prod_pow Fin.prod_univ_succ Finset.prod_congr MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Polynomial.coeff_C_mul coeff_C_mul coeff_monomial mul_boole mul_comm Polynomial.coeff_C_mul_X_pow eq_or_ne monomial_eq one_mul ne_or_eq Finsupp.cons_tail map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Polynomial.coeff_add coeff_add
finSuccEquiv_comp_C_eq_C 📖	mathematical	—	RingHom.comp Polynomial MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Semiring.toNonAssocSemiring Polynomial.semiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHomClass.toRingHom AlgEquiv Polynomial.algebraOfAlgebra AddMonoidAlgebra.algebra Algebra.id AlgEquiv.instFunLike AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass AlgEquiv.symm finSuccEquiv Polynomial.C C	—	RingHom.ext AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass RingHom.comp_apply AlgEquiv.injective AlgEquiv.apply_symm_apply finSuccEquiv_apply eval₂Hom_C
finSuccEquiv_eq 📖	mathematical	—	RingHomClass.toRingHom AlgEquiv MvPolynomial Polynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass finSuccEquiv eval₂Hom Polynomial.commSemiring AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid RingHom.comp Polynomial.C C Polynomial.X DFunLike.coe RingHom RingHom.instFunLike X	—	ringHom_ext' AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass RingHom.ext rename_C aeval_C eval₂_C Polynomial.ext rename_X aeval_X eval₂Hom_X' finSuccEquiv_succ
finSuccEquiv_rename_finSuccEquiv 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv AlgHom AlgHom.funLike rename Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.trans Equiv.optionCongr Equiv.symm finSuccEquiv Polynomial.map AlgHom.toRingHom optionEquivLeft	—	AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass ringHom_ext algHom_C finSuccEquiv_apply eval₂Hom_C AlgHom.algHomClass Polynomial.map_C rename_X finSuccEquiv_symm_none eval₂Hom_X' aeval_X Polynomial.map_X finSuccEquiv_symm_some DFunLike.congr_fun
image_support_finSuccEquiv 📖	mathematical	—	Finset.image Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instDecidableEq Finsupp.cons support Polynomial.coeff MvPolynomial AddMonoidAlgebra.semiring CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv Finset.filter Finsupp.instFunLike	—	Finset.ext Finset.mem_filter Finset.mem_image mem_support_iff finSuccEquiv_coeff_coeff Finsupp.cons_tail
isEmptyAlgEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgEquiv.instFunLike isEmptyAlgEquiv RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Semiring.toNonAssocSemiring RingHom.instFunLike eval isEmptyElim	—	—
isEmptyRingEquiv_apply 📖	mathematical	—	DFunLike.coe RingEquiv MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd AddMonoidAlgebra.nonUnitalNonAssocSemiring EquivLike.toFunLike RingEquiv.instEquivLike isEmptyRingEquiv RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass RingHom.instFunLike eval isEmptyElim	—	—
isEmptyRingEquiv_eq_coeff_zero 📖	mathematical	—	DFunLike.coe RingEquiv MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd AddMonoidAlgebra.nonUnitalNonAssocSemiring EquivLike.toFunLike RingEquiv.instEquivLike isEmptyRingEquiv coeff Finsupp.instZero	—	RingEquiv.surjective eval_C IsEmpty.instSubsingleton coeff_C
isEmptyRingEquiv_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid Distrib.toAdd AddMonoidAlgebra.nonUnitalNonAssocSemiring EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm isEmptyRingEquiv RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass RingHom.instFunLike C	—	—
isEmptyRingEquiv_symm_toRingHom 📖	mathematical	—	RingEquiv.toRingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingEquiv.symm AddMonoidAlgebra.instMul Finsupp.instAdd Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd AddMonoidAlgebra.nonUnitalNonAssocSemiring isEmptyRingEquiv C	—	—
iterToSum_C_C 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.nonAssocSemiring CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike iterToSum Semiring.toNonAssocSemiring C	—	eval₂_C
iterToSum_C_X 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.nonAssocSemiring CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike iterToSum Semiring.toNonAssocSemiring C X	—	eval₂_C eval₂_X
iterToSum_X 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.nonAssocSemiring CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike iterToSum X	—	eval₂_X
iterToSum_sumToIter 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.nonAssocSemiring CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike iterToSum sumToIter	—	RingEquiv.symm_apply_apply
mapAlgEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra AlgEquiv.instFunLike mapAlgEquiv RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike map RingHomClass.toRingHom Semiring.toNonAssocSemiring	—	—
mapAlgEquiv_refl 📖	mathematical	—	mapAlgEquiv AlgEquiv.refl CommSemiring.toSemiring MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra	—	AlgEquiv.ext map_id
mapAlgEquiv_symm 📖	mathematical	—	AlgEquiv.symm MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra mapAlgEquiv	—	—
mapAlgEquiv_trans 📖	mathematical	—	AlgEquiv.trans MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra mapAlgEquiv	—	AlgEquiv.ext ext map_map
mapEquiv_apply 📖	mathematical	—	DFunLike.coe RingEquiv MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidAlgebra.nonUnitalNonAssocSemiring EquivLike.toFunLike RingEquiv.instEquivLike mapEquiv RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass RingHom.instFunLike map RingHomClass.toRingHom Distrib.toMul NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—
mapEquiv_refl 📖	mathematical	—	mapEquiv RingEquiv.refl Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidAlgebra.nonUnitalNonAssocSemiring	—	RingEquiv.ext map_id
mapEquiv_symm 📖	mathematical	—	RingEquiv.symm MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidAlgebra.nonUnitalNonAssocSemiring mapEquiv Distrib.toMul NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—
mapEquiv_trans 📖	mathematical	—	RingEquiv.trans MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidAlgebra.nonUnitalNonAssocSemiring mapEquiv Distrib.toMul NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	RingEquiv.ext RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass map_map
mem_image_support_coeff_finSuccEquiv 📖	mathematical	—	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Set Set.instMembership Set.image Finsupp.cons SetLike.coe Finset Finset.instSetLike support Polynomial.coeff MvPolynomial AddMonoidAlgebra.semiring CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv SetLike.instMembership Finsupp.instFunLike	—	image_support_finSuccEquiv
mem_support_coeff_finSuccEquiv 📖	mathematical	—	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset SetLike.instMembership Finset.instSetLike support Polynomial.coeff MvPolynomial AddMonoidAlgebra.semiring CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv Finsupp.cons	—	finSuccEquiv_coeff_coeff
mem_support_coeff_optionEquivLeft 📖	mathematical	—	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset SetLike.instMembership Finset.instSetLike support Polynomial.coeff MvPolynomial AddMonoidAlgebra.semiring CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft Finsupp.optionElim	—	Finsupp.some_optionElim Finsupp.optionElim_apply_eq_elim
mem_support_finSuccEquiv 📖	mathematical	—	Finset SetLike.instMembership Finset.instSetLike Polynomial.support MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv Set Set.instMembership Set.image Finsupp.instFunLike SetLike.coe support	—	support_finSuccEquiv
mvPolynomialEquivMvPolynomial_apply 📖	mathematical	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid C DFunLike.coe RingHom RingHom.instFunLike X	DFunLike.coe RingEquiv MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidAlgebra.nonUnitalNonAssocSemiring EquivLike.toFunLike RingEquiv.instEquivLike mvPolynomialEquivMvPolynomial RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass RingHom.instFunLike	—	—
mvPolynomialEquivMvPolynomial_symm_apply 📖	mathematical	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid C DFunLike.coe RingHom RingHom.instFunLike X	DFunLike.coe RingEquiv MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidAlgebra.nonUnitalNonAssocSemiring EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm mvPolynomialEquivMvPolynomial RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass RingHom.instFunLike	—	—
natDegree_finSuccEquiv 📖	mathematical	—	Polynomial.natDegree MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv degreeOf	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Polynomial.natDegree_zero degreeOf_zero Polynomial.natDegree.eq_1 degree_finSuccEquiv Nat.cast_withBot WithBot.unbotD_coe
natDegree_optionEquivLeft 📖	mathematical	—	Polynomial.natDegree MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft degreeOf	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Polynomial.natDegree_zero degreeOf_zero Polynomial.natDegree.eq_1 degree_optionEquivLeft Nat.cast_withBot WithBot.unbotD_coe
nonempty_support_finSuccEquiv 📖	mathematical	—	Finset.Nonempty Polynomial.support MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv	—	Polynomial.support_nonempty EmbeddingLike.map_ne_zero_iff EquivLike.toEmbeddingLike MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass
nonempty_support_optionEquivLeft 📖	mathematical	—	Finset.Nonempty Polynomial.support MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft	—	Polynomial.support_nonempty EmbeddingLike.map_ne_zero_iff EquivLike.toEmbeddingLike MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass
optionEquivLeft_C 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike C Polynomial.C	—	aeval_C
optionEquivLeft_X_none 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft X Polynomial.X	—	aeval_X
optionEquivLeft_X_some 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft X RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	—	aeval_X
optionEquivLeft_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft AlgHom AlgHom.funLike aeval Polynomial.commSemiring AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid Polynomial.X RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C X	—	—
optionEquivLeft_coeff_coeff 📖	mathematical	—	coeff Polynomial.coeff MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft Finsupp.optionElim	—	optionEquivLeft_coeff_some_coeff_none Finsupp.some_optionElim Finsupp.optionElim_apply_eq_elim
optionEquivLeft_coeff_some_coeff_none 📖	mathematical	—	coeff Finsupp.some MulZeroClass.toZero Nat.instMulZeroClass Polynomial.coeff MvPolynomial AddMonoidAlgebra.semiring Finsupp CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft Finsupp.instFunLike	—	induction_on' optionEquivLeft_monomial Polynomial.coeff_monomial coeff_monomial map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Polynomial.coeff_add coeff_add
optionEquivLeft_elim_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 Polynomial.eval Polynomial.map AddMonoidAlgebra.semiring Finsupp.instAddMonoid AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft	—	eval_C Polynomial.map_C algHom_ext aeval_X Polynomial.map_X Polynomial.eval_X eval_X Polynomial.eval_C
optionEquivLeft_monomial 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike monomial Polynomial.module Polynomial.monomial Finsupp.instFunLike Finsupp.some	—	optionEquivLeft_apply aeval_monomial Finsupp.prod_option_index pow_zero pow_add monomial_eq Polynomial.C_mul_X_pow_eq_monomial map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mul_assoc mul_comm map_finsuppProd MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_pow
optionEquivLeft_symm_C_C 📖	mathematical	—	DFunLike.coe AlgEquiv Polynomial MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.semiring Polynomial.algebraOfAlgebra AddMonoidAlgebra.algebra Algebra.id AlgEquiv.instFunLike AlgEquiv.symm optionEquivLeft RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass C	—	Polynomial.aevalTower_C algHom_C
optionEquivLeft_symm_C_X 📖	mathematical	—	DFunLike.coe AlgEquiv Polynomial MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.semiring Polynomial.algebraOfAlgebra AddMonoidAlgebra.algebra Algebra.id AlgEquiv.instFunLike AlgEquiv.symm optionEquivLeft RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C X	—	Polynomial.aevalTower_C rename_X
optionEquivLeft_symm_X 📖	mathematical	—	DFunLike.coe AlgEquiv Polynomial MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.semiring Polynomial.algebraOfAlgebra AddMonoidAlgebra.algebra Algebra.id AlgEquiv.instFunLike AlgEquiv.symm optionEquivLeft Polynomial.X X	—	Polynomial.aevalTower_X
optionEquivLeft_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Polynomial MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.semiring Polynomial.algebraOfAlgebra AddMonoidAlgebra.algebra Algebra.id AlgEquiv.instFunLike AlgEquiv.symm optionEquivLeft AlgHom AlgHom.funLike Polynomial.aevalTower AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid rename X	—	—
optionEquivRight_C 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial CommSemiring.toSemiring Polynomial.commSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivRight RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike C Polynomial.semiring Polynomial.C	—	aeval_C
optionEquivRight_X_none 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial CommSemiring.toSemiring Polynomial.commSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivRight X RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike C Polynomial.X	—	aeval_X
optionEquivRight_X_some 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial CommSemiring.toSemiring Polynomial.commSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivRight X	—	aeval_X
optionEquivRight_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial CommSemiring.toSemiring Polynomial.commSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivRight AlgHom AlgHom.funLike aeval AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike C Polynomial.X X	—	—
optionEquivRight_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial CommSemiring.toSemiring Polynomial.commSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Polynomial.algebraOfAlgebra Algebra.id AlgEquiv.instFunLike AlgEquiv.symm optionEquivRight AlgHom AlgHom.funLike aevalTower AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid Polynomial.aeval X	—	—
pUnitAlgEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial CommSemiring.toSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike pUnitAlgEquiv eval₂ Polynomial.commSemiring Polynomial.C Polynomial.X	—	—
pUnitAlgEquiv_monomial 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial CommSemiring.toSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike pUnitAlgEquiv LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike monomial Polynomial.module Polynomial.monomial Finsupp.instFunLike	—	eval₂_monomial Finsupp.prod_pow Finset.prod_congr Finset.univ_unique Finset.prod_singleton Polynomial.C_mul_X_pow_eq_monomial
pUnitAlgEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Polynomial CommSemiring.toSemiring MvPolynomial Polynomial.semiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.algebraOfAlgebra Algebra.id AddMonoidAlgebra.algebra AlgEquiv.instFunLike AlgEquiv.symm pUnitAlgEquiv Polynomial.eval₂ C X	—	—
pUnitAlgEquiv_symm_monomial 📖	mathematical	—	DFunLike.coe AlgEquiv Polynomial CommSemiring.toSemiring MvPolynomial Polynomial.semiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.algebraOfAlgebra Algebra.id AddMonoidAlgebra.algebra AlgEquiv.instFunLike AlgEquiv.symm pUnitAlgEquiv LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Polynomial.module LinearMap.instFunLike Polynomial.monomial Finsupp.instFunLike AddMonoidAlgebra.addAddCommMonoid AddMonoidAlgebra.module monomial	—	Polynomial.eval₂_monomial monomial_eq Finsupp.prod_pow Finset.prod_congr Finset.univ_unique Finset.prod_singleton
rename_comp_toMvPolynomial 📖	mathematical	—	AlgHom.comp Polynomial CommSemiring.toSemiring MvPolynomial Polynomial.semiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid Polynomial.algebraOfAlgebra Algebra.id AddMonoidAlgebra.algebra rename Polynomial.toMvPolynomial	—	Polynomial.algHom_ext ext Polynomial.toMvPolynomial_X rename_X
rename_polynomial_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 rename Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Polynomial.aeval X	—	Polynomial.aeval_algHom_apply AlgHom.algHomClass rename_X
rename_toMvPolynomial 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike rename Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Polynomial.toMvPolynomial	—	DFunLike.congr_fun rename_comp_toMvPolynomial
sumAlgEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.semiring CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid AlgEquiv.instFunLike sumAlgEquiv RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike sumToIter	—	—
sumAlgEquiv_comp_rename_inl 📖	mathematical	—	AlgHom.comp MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.semiring CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid AlgEquiv.toAlgHom sumAlgEquiv rename mapAlgHom Algebra.ofId	—	algHom_ext ext rename_X sumToIter_Xl eval₂_X
sumAlgEquiv_comp_rename_inr 📖	mathematical	—	AlgHom.comp MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.semiring CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid AlgEquiv.toAlgHom sumAlgEquiv rename IsScalarTower.toAlgHom 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_ext AddMonoidAlgebra.isScalarTower IsScalarTower.right ext rename_X sumToIter_Xr
sumAlgEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.semiring CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid AlgEquiv.instFunLike AlgEquiv.symm sumAlgEquiv RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike iterToSum	—	—
sumToIter_C 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.nonAssocSemiring CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike sumToIter Semiring.toNonAssocSemiring C	—	eval₂_C
sumToIter_Xl 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.nonAssocSemiring CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike sumToIter X	—	eval₂_X
sumToIter_Xr 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.nonAssocSemiring CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike sumToIter X Semiring.toNonAssocSemiring C	—	eval₂_X
sumToIter_iterToSum 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.nonAssocSemiring CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike sumToIter iterToSum	—	RingEquiv.apply_symm_apply
support_coeff_finSuccEquiv 📖	mathematical	—	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset SetLike.instMembership Finset.instSetLike support Polynomial.coeff MvPolynomial AddMonoidAlgebra.semiring CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv Finsupp.cons	—	mem_support_coeff_finSuccEquiv
support_finSuccEquiv 📖	mathematical	—	Polynomial.support MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv Finset.image Finsupp.instFunLike support	—	Finset.ext Polynomial.mem_support_iff Finset.mem_image Finsupp.ne_iff mem_support_coeff_finSuccEquiv Finsupp.cons_zero coeff.eq_1 Finsupp.zero_apply mem_support_iff Finsupp.cons_tail
support_finSuccEquiv_nonempty 📖	mathematical	—	Finset.Nonempty Polynomial.support MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv	—	nonempty_support_finSuccEquiv
support_optionEquivLeft 📖	mathematical	—	Polynomial.support MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft Finset.image Finsupp.instFunLike support	—	Finset.ext Polynomial.mem_support_iff Finset.mem_image Finsupp.ne_iff mem_support_coeff_optionEquivLeft Finsupp.optionElim_apply_none coeff.eq_1 Finsupp.zero_apply mem_support_iff Finsupp.optionElim_some
totalDegree_coeff_finSuccEquiv_add_le 📖	mathematical	—	totalDegree Polynomial.coeff MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv	—	Finset.nonempty_iff_ne_empty support_eq_empty Finset.exists_mem_eq_sup totalDegree.eq_1 Finsupp.sum_cons add_comm le_totalDegree mem_support_coeff_finSuccEquiv
totalDegree_coeff_optionEquivLeft_add_le 📖	mathematical	totalDegree	totalDegree Polynomial.coeff MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft	—	totalDegree_zero zero_add totalDegree.eq_1 add_comm Finset.add_sup Nat.instCanonicallyOrderedAdd IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub Finset.sup_le_iff le_trans Finsupp.sum_add_index Finsupp.sum_embDomain Finsupp.sum_single_index instReflLe Finset.le_sup optionEquivLeft_coeff_some_coeff_none Finsupp.some_add Finsupp.some_embDomain_some Finsupp.some_single_none add_zero Finsupp.embDomain_some_none Finsupp.single_eq_same
totalDegree_coeff_optionEquivLeft_le 📖	mathematical	—	totalDegree Polynomial.coeff MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe AlgEquiv Polynomial Polynomial.semiring AddMonoidAlgebra.algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft	—	totalDegree_zero Nat.instCanonicallyOrderedAdd totalDegree.eq_1 Finset.sup_le_iff le_trans Finsupp.sum_add_index Finsupp.sum_embDomain Finsupp.sum_single_index IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le Finset.le_sup optionEquivLeft_coeff_some_coeff_none Finsupp.some_add Finsupp.some_embDomain_some Finsupp.some_single_none add_zero Finsupp.embDomain_some_none Finsupp.single_eq_same zero_add

Polynomial

Definitions

Name	Category	Theorems
toMvPolynomial 📖	CompOp	10 math math: MvPolynomial.eval_comp_toMvPolynomial, toMvPolynomial_eq_rename_comp, MvPolynomial.aeval_toMvPolynomial, MvPolynomial.rename_comp_toMvPolynomial, toMvPolynomial_X, MvPolynomial.eval_toMvPolynomial, MvPolynomial.rename_toMvPolynomial, toMvPolynomial_injective, MvPolynomial.aeval_comp_toMvPolynomial, toMvPolynomial_C

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMvPolynomial_C 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring MvPolynomial semiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid algebraOfAlgebra Algebra.id AddMonoidAlgebra.algebra AlgHom.funLike toMvPolynomial RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass MvPolynomial.C	—	aeval_C
toMvPolynomial_X 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring MvPolynomial semiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid algebraOfAlgebra Algebra.id AddMonoidAlgebra.algebra AlgHom.funLike toMvPolynomial X MvPolynomial.X	—	aeval_X
toMvPolynomial_eq_rename_comp 📖	mathematical	—	toMvPolynomial AlgHom.comp Polynomial CommSemiring.toSemiring MvPolynomial semiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid algebraOfAlgebra Algebra.id AddMonoidAlgebra.algebra MvPolynomial.rename AlgHomClass.toAlgHom AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass AlgEquiv.symm MvPolynomial.pUnitAlgEquiv	—	algHom_ext AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass MvPolynomial.ext toMvPolynomial_X eval₂_X MvPolynomial.rename_X
toMvPolynomial_injective 📖	mathematical	—	Polynomial CommSemiring.toSemiring MvPolynomial DFunLike.coe AlgHom semiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid algebraOfAlgebra Algebra.id AddMonoidAlgebra.algebra AlgHom.funLike toMvPolynomial	—	AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass toMvPolynomial_eq_rename_comp MvPolynomial.rename_injective

---

← Back to Index