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 commSemiring Polynomial.algebraOfAlgebra Algebra.id 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 CommSemiring.toSemiring commSemiring 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 CommSemiring.toSemiring commSemiring 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 commSemiring eval DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	Polynomial.coeff_map
commAlgEquiv_C 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial commSemiring CommSemiring.toSemiring algebra Algebra.id AlgEquiv.instFunLike commAlgEquiv RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C map	—	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 commSemiring CommSemiring.toSemiring algebra Algebra.id AlgEquiv.instFunLike commAlgEquiv RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C X	—	commAlgEquiv_C map_X
commAlgEquiv_X 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial commSemiring CommSemiring.toSemiring algebra Algebra.id AlgEquiv.instFunLike commAlgEquiv X RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	iterToSum_X rename_X sumToIter_Xr
degreeOf_coeff_finSuccEquiv 📖	mathematical	—	degreeOf Polynomial.coeff MvPolynomial CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring 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 CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring 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 CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv WithBot AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne 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 CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft WithBot AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne 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 commSemiring eval RingHomClass.toRingHom AlgHom Polynomial.algebraOfAlgebra Algebra.id 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval Fin.cons Polynomial.eval Polynomial.map AlgEquiv Polynomial Polynomial.semiring 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval AlgHom Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id 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 commSemiring Polynomial.semiring 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 commSemiring Polynomial.algebraOfAlgebra Algebra.id algebra AlgEquiv.instFunLike AlgEquiv.symm pUnitAlgEquiv Polynomial.eval₂	—	eval₂_pUnitAlgEquiv_symm
eval₂_pUnitAlgEquiv 📖	mathematical	—	Polynomial.eval₂ CommSemiring.toSemiring DFunLike.coe AlgEquiv MvPolynomial Polynomial commSemiring Polynomial.semiring 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 commSemiring Polynomial.algebraOfAlgebra Algebra.id 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 CommSemiring.toSemiring commSemiring Polynomial.semiring 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 CommSemiring.toSemiring commSemiring Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv X Polynomial.X	—	finSuccEquiv_apply eval₂Hom_X'
finSuccEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial CommSemiring.toSemiring commSemiring Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv RingHom Semiring.toNonAssocSemiring Polynomial.commSemiring 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 CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv Finsupp.cons MulZeroClass.toZero Nat.instMulZeroClass	—	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 CommSemiring.toSemiring commSemiring Semiring.toNonAssocSemiring Polynomial.semiring RingHomClass.toRingHom AlgEquiv Polynomial.algebraOfAlgebra 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 CommSemiring.toSemiring commSemiring Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass finSuccEquiv eval₂Hom Polynomial.commSemiring 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 CommSemiring.toSemiring commSemiring Polynomial.semiring 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 CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring 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 CommSemiring.toSemiring commSemiring algebra Algebra.id AlgEquiv.instFunLike isEmptyAlgEquiv RingHom Semiring.toNonAssocSemiring RingHom.instFunLike eval isEmptyElim	—	—
isEmptyRingEquiv_apply 📖	mathematical	—	DFunLike.coe RingEquiv MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike isEmptyRingEquiv RingHom RingHom.instFunLike eval isEmptyElim	—	—
isEmptyRingEquiv_eq_coeff_zero 📖	mathematical	—	DFunLike.coe RingEquiv MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike isEmptyRingEquiv coeff Finsupp MulZeroClass.toZero Nat.instMulZeroClass 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 commSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm isEmptyRingEquiv RingHom RingHom.instFunLike C	—	—
isEmptyRingEquiv_symm_toRingHom 📖	mathematical	—	RingEquiv.toRingHom MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingEquiv.symm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd isEmptyRingEquiv C	—	—
iterToSum_C_C 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial commSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike iterToSum C	—	eval₂_C
iterToSum_C_X 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial commSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike iterToSum C X	—	eval₂_C eval₂_X
iterToSum_X 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial commSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike iterToSum X	—	eval₂_X
iterToSum_sumToIter 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial commSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike iterToSum sumToIter	—	RingEquiv.symm_apply_apply
mapAlgEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial CommSemiring.toSemiring commSemiring algebra AlgEquiv.instFunLike mapAlgEquiv RingHom Semiring.toNonAssocSemiring RingHom.instFunLike map RingHomClass.toRingHom	—	—
mapAlgEquiv_refl 📖	mathematical	—	mapAlgEquiv AlgEquiv.refl CommSemiring.toSemiring MvPolynomial commSemiring algebra	—	AlgEquiv.ext map_id
mapAlgEquiv_symm 📖	mathematical	—	AlgEquiv.symm MvPolynomial CommSemiring.toSemiring commSemiring algebra mapAlgEquiv	—	—
mapAlgEquiv_trans 📖	mathematical	—	AlgEquiv.trans MvPolynomial CommSemiring.toSemiring commSemiring algebra mapAlgEquiv	—	AlgEquiv.ext ext map_map
mapEquiv_apply 📖	mathematical	—	DFunLike.coe RingEquiv MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike mapEquiv RingHom RingHom.instFunLike map RingHomClass.toRingHom	—	—
mapEquiv_refl 📖	mathematical	—	mapEquiv RingEquiv.refl Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toAdd MvPolynomial commSemiring	—	RingEquiv.ext map_id
mapEquiv_symm 📖	mathematical	—	RingEquiv.symm MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Distrib.toAdd mapEquiv	—	—
mapEquiv_trans 📖	mathematical	—	RingEquiv.trans MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Distrib.toAdd mapEquiv	—	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 CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv Finset.instMembership Finsupp.instFunLike	—	image_support_finSuccEquiv
mem_support_coeff_finSuccEquiv 📖	mathematical	—	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset Finset.instMembership support Polynomial.coeff MvPolynomial CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv Finsupp.cons	—	finSuccEquiv_coeff_coeff
mem_support_coeff_optionEquivLeft 📖	mathematical	—	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset Finset.instMembership support Polynomial.coeff MvPolynomial CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft Finsupp.optionElim	—	Finsupp.some_optionElim Finsupp.optionElim_apply_eq_elim
mem_support_finSuccEquiv 📖	mathematical	—	Finset Finset.instMembership Polynomial.support MvPolynomial CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv Set Set.instMembership Set.image Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instFunLike SetLike.coe Finset.instSetLike support	—	support_finSuccEquiv
mvPolynomialEquivMvPolynomial_apply 📖	mathematical	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring C DFunLike.coe RingHom RingHom.instFunLike X	RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike mvPolynomialEquivMvPolynomial	—	—
mvPolynomialEquivMvPolynomial_symm_apply 📖	mathematical	RingHom.comp MvPolynomial Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring C DFunLike.coe RingHom RingHom.instFunLike X	RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm mvPolynomialEquivMvPolynomial	—	—
natDegree_finSuccEquiv 📖	mathematical	—	Polynomial.natDegree MvPolynomial CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring 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 CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring 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 CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring 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 CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring 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 CommSemiring.toSemiring commSemiring Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C Polynomial.C	—	aeval_C
optionEquivLeft_X_none 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial CommSemiring.toSemiring commSemiring Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft X Polynomial.X	—	aeval_X
optionEquivLeft_X_some 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial CommSemiring.toSemiring commSemiring Polynomial.semiring 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 CommSemiring.toSemiring commSemiring Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft AlgHom AlgHom.funLike aeval Polynomial.commSemiring Polynomial.X RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C X	—	—
optionEquivLeft_coeff_coeff 📖	mathematical	—	coeff Polynomial.coeff MvPolynomial CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft Finsupp.optionElim MulZeroClass.toZero Nat.instMulZeroClass	—	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 CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft Finsupp 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval Polynomial.eval Polynomial.map AlgEquiv Polynomial Polynomial.semiring 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 CommSemiring.toSemiring commSemiring Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial Polynomial.module Polynomial.monomial Finsupp MulZeroClass.toZero Nat.instMulZeroClass 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 CommSemiring.toSemiring commSemiring Polynomial.semiring Polynomial.algebraOfAlgebra algebra Algebra.id AlgEquiv.instFunLike AlgEquiv.symm optionEquivLeft RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C C	—	Polynomial.aevalTower_C algHom_C
optionEquivLeft_symm_C_X 📖	mathematical	—	DFunLike.coe AlgEquiv Polynomial MvPolynomial CommSemiring.toSemiring commSemiring Polynomial.semiring Polynomial.algebraOfAlgebra 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 CommSemiring.toSemiring commSemiring Polynomial.semiring Polynomial.algebraOfAlgebra algebra Algebra.id AlgEquiv.instFunLike AlgEquiv.symm optionEquivLeft Polynomial.X X	—	Polynomial.aevalTower_X
optionEquivLeft_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Polynomial MvPolynomial CommSemiring.toSemiring commSemiring Polynomial.semiring Polynomial.algebraOfAlgebra algebra Algebra.id AlgEquiv.instFunLike AlgEquiv.symm optionEquivLeft AlgHom AlgHom.funLike Polynomial.aevalTower rename X	—	—
optionEquivRight_C 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial CommSemiring.toSemiring Polynomial.commSemiring commSemiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivRight RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C Polynomial.semiring Polynomial.C	—	aeval_C
optionEquivRight_X_none 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial CommSemiring.toSemiring Polynomial.commSemiring commSemiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivRight X RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C Polynomial.X	—	aeval_X
optionEquivRight_X_some 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial CommSemiring.toSemiring Polynomial.commSemiring commSemiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivRight X	—	aeval_X
optionEquivRight_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial CommSemiring.toSemiring Polynomial.commSemiring commSemiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivRight AlgHom AlgHom.funLike aeval RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C Polynomial.X X	—	—
optionEquivRight_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial CommSemiring.toSemiring Polynomial.commSemiring commSemiring algebra Polynomial.algebraOfAlgebra Algebra.id AlgEquiv.instFunLike AlgEquiv.symm optionEquivRight AlgHom AlgHom.funLike aevalTower Polynomial.aeval X	—	—
pUnitAlgEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial Polynomial CommSemiring.toSemiring commSemiring Polynomial.semiring 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 commSemiring Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike pUnitAlgEquiv LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial Polynomial.module Polynomial.monomial Finsupp MulZeroClass.toZero Nat.instMulZeroClass 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 commSemiring Polynomial.algebraOfAlgebra Algebra.id algebra AlgEquiv.instFunLike AlgEquiv.symm pUnitAlgEquiv Polynomial.eval₂ C X	—	—
pUnitAlgEquiv_symm_monomial 📖	mathematical	—	DFunLike.coe AlgEquiv Polynomial CommSemiring.toSemiring MvPolynomial Polynomial.semiring commSemiring Polynomial.algebraOfAlgebra Algebra.id algebra AlgEquiv.instFunLike AlgEquiv.symm pUnitAlgEquiv LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Polynomial.module LinearMap.instFunLike Polynomial.monomial Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instFunLike 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 commSemiring Polynomial.algebraOfAlgebra Algebra.id algebra rename Polynomial.toMvPolynomial	—	Polynomial.algHom_ext ext Polynomial.toMvPolynomial_X rename_X
rename_polynomial_aeval_X 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring 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 CommSemiring.toSemiring commSemiring 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 commSemiring CommSemiring.toSemiring algebra Algebra.id AlgEquiv.instFunLike sumAlgEquiv RingHom Semiring.toNonAssocSemiring RingHom.instFunLike sumToIter	—	—
sumAlgEquiv_comp_rename_inl 📖	mathematical	—	AlgHom.comp MvPolynomial commSemiring CommSemiring.toSemiring algebra Algebra.id AlgEquiv.toAlgHom sumAlgEquiv rename mapAlgHom Algebra.ofId	—	algHom_ext ext rename_X sumToIter_Xl eval₂_X
sumAlgEquiv_comp_rename_inr 📖	mathematical	—	AlgHom.comp MvPolynomial commSemiring CommSemiring.toSemiring algebra Algebra.id AlgEquiv.toAlgHom sumAlgEquiv rename IsScalarTower.toAlgHom 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_ext isScalarTower IsScalarTower.right ext rename_X sumToIter_Xr
sumAlgEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial commSemiring CommSemiring.toSemiring algebra Algebra.id AlgEquiv.instFunLike AlgEquiv.symm sumAlgEquiv RingHom Semiring.toNonAssocSemiring RingHom.instFunLike iterToSum	—	—
sumToIter_C 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial commSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike sumToIter C	—	eval₂_C
sumToIter_Xl 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial commSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike sumToIter X	—	eval₂_X
sumToIter_Xr 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial commSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike sumToIter X C	—	eval₂_X
sumToIter_iterToSum 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial commSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike sumToIter iterToSum	—	RingEquiv.apply_symm_apply
support_coeff_finSuccEquiv 📖	mathematical	—	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finset Finset.instMembership support Polynomial.coeff MvPolynomial CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv Finsupp.cons	—	mem_support_coeff_finSuccEquiv
support_finSuccEquiv 📖	mathematical	—	Polynomial.support MvPolynomial CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv Finset.image Finsupp MulZeroClass.toZero Nat.instMulZeroClass 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 CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike finSuccEquiv	—	nonempty_support_finSuccEquiv
support_optionEquivLeft 📖	mathematical	—	Polynomial.support MvPolynomial CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring algebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike optionEquivLeft Finset.image Finsupp MulZeroClass.toZero Nat.instMulZeroClass 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 CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring 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	Polynomial.coeff MvPolynomial CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring 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 AddLeftCancelSemigroup.toIsLeftCancelAdd 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 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 CommSemiring.toSemiring commSemiring DFunLike.coe AlgEquiv Polynomial Polynomial.semiring 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 AddLeftCancelSemigroup.toIsLeftCancelAdd 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 MvPolynomial.commSemiring algebraOfAlgebra Algebra.id MvPolynomial.algebra AlgHom.funLike toMvPolynomial RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C MvPolynomial.C	—	aeval_C
toMvPolynomial_X 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring MvPolynomial semiring MvPolynomial.commSemiring algebraOfAlgebra Algebra.id MvPolynomial.algebra AlgHom.funLike toMvPolynomial X MvPolynomial.X	—	aeval_X
toMvPolynomial_eq_rename_comp 📖	mathematical	—	toMvPolynomial AlgHom.comp Polynomial CommSemiring.toSemiring MvPolynomial semiring MvPolynomial.commSemiring algebraOfAlgebra Algebra.id MvPolynomial.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 MvPolynomial.commSemiring algebraOfAlgebra Algebra.id MvPolynomial.algebra AlgHom.funLike toMvPolynomial	—	AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass toMvPolynomial_eq_rename_comp MvPolynomial.rename_injective

---

← Back to Index