Degree

📁 Source: Mathlib/Algebra/Polynomial/Eval/Degree.lean

Statistics

Metric	Count
Definitions mapEquiv	1
Theorems coeff_comp_degree_mul_degree, comp_C_mul_X_coeff, comp_C_mul_X_eq_zero_iff, degree_map_eq_of_leadingCoeff_ne_zero, degree_map_le, degree_map_lt, eval_eq_sum_range, eval_eq_sum_range', eval_monomial_one_add_sub, eval₂_comp, eval₂_eq_sum_range, eval₂_eq_sum_range', isUnit_of_isUnit_leadingCoeff_of_isUnit_map, iterate_comp_eval, iterate_comp_eval₂, leadingCoeff_map_of_leadingCoeff_ne_zero, mapEquiv_apply, mapEquiv_symm_apply, map_monic_eq_zero_iff, map_monic_ne_zero, natDegree_map_le, natDegree_map_lt, natDegree_map_lt', natDegree_map_of_leadingCoeff_ne_zero, nextCoeff_map_of_leadingCoeff_ne_zero	25
Total	26

Polynomial

Definitions

Name	Category	Theorems
mapEquiv 📖	CompOp	2 math math: mapEquiv_symm_apply, mapEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_comp_degree_mul_degree 📖	mathematical	—	coeff comp natDegree Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring leadingCoeff Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	comp.eq_1 eval₂_def coeff_sum Finset.sum_eq_single coeff_eq_zero_of_natDegree_lt LE.le.trans_lt natDegree_mul_le natDegree_C zero_add natDegree_pow_le mul_lt_mul_of_pos_right IsStrictOrderedRing.toMulPosStrictMono Nat.instIsStrictOrderedRing lt_of_le_of_ne le_natDegree_of_mem_supp lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass pow_zero mul_one MulZeroClass.zero_mul coeff_C_mul coeff_pow_mul_natDegree
comp_C_mul_X_coeff 📖	mathematical	—	coeff comp Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C X Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	eval₂_eq_sum_range Finset.sum_congr Commute.mul_pow Commute.symm commute_X finset_sum_coeff coeff_C_mul coeff_X_pow Finset.sum_eq_single MulZeroClass.mul_zero coeff_eq_zero_of_natDegree_lt not_le Finset.mem_range_succ_iff MulZeroClass.zero_mul mul_one
comp_C_mul_X_eq_zero_iff 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	comp Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C X instZero	—	comp_C_mul_X_coeff coeff_zero mul_right_mem_nonZeroDivisors_eq_zero_iff pow_mem Submonoid.instSubmonoidClass
degree_map_eq_of_leadingCoeff_ne_zero 📖	mathematical	—	degree map	—	LE.le.antisymm degree_map_le leadingCoeff_ne_zero trans IsPreorder.toIsTrans IsEquiv.toIsPreorder eq_isEquiv RingHom.map_zero degree_eq_natDegree le_degree_of_ne_zero coeff_map
degree_map_le 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree map	—	degree_le_iff_coeff_zero coeff_map degree_lt_iff_coeff_zero le_rfl map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
degree_map_lt 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike leadingCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree map	—	LE.le.lt_of_ne degree_map_le degree_eq_bot leadingCoeff_eq_zero leadingCoeff.eq_1 natDegree_eq_natDegree coeff_map degree_zero
eval_eq_sum_range 📖	mathematical	—	eval Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.range natDegree Distrib.toMul NonUnitalNonAssocSemiring.toDistrib coeff Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	eval_eq_sum sum_over_range MulZeroClass.zero_mul
eval_eq_sum_range' 📖	mathematical	natDegree	eval Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.range Distrib.toMul NonUnitalNonAssocSemiring.toDistrib coeff Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	eval_eq_sum sum_over_range' MulZeroClass.zero_mul
eval_monomial_one_add_sub 📖	mathematical	—	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing eval CommSemiring.toSemiring CommRing.toCommSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Semiring.toModule module LinearMap.instFunLike monomial AddMonoidWithOne.toNatCast Finset.sum Finset.range Distrib.toMul Nat.choose Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Nat.cast_succ eval_monomial add_comm add_pow Finset.sum_congr one_pow mul_one mul_comm Finset.sum_range_succ mul_add Distrib.leftDistribClass Nat.choose_self Nat.cast_one one_mul add_sub_cancel_right Finset.mul_sum Finset.sum_range_succ' Nat.cast_zero MulZeroClass.zero_mul MulZeroClass.mul_zero add_zero mul_assoc Nat.cast_mul Nat.add_one_mul_choose_eq
eval₂_comp 📖	mathematical	—	eval₂ CommSemiring.toSemiring comp	—	comp.eq_1 as_sum_range eval₂_finset_sum Finset.sum_congr eval₂_monomial eval₂_mul eval₂_C eval₂_pow
eval₂_eq_sum_range 📖	mathematical	—	eval₂ Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.range natDegree Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe RingHom RingHom.instFunLike coeff Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	trans IsPreorder.toIsTrans IsEquiv.toIsPreorder eq_isEquiv as_sum_range eval₂_finset_sum eval₂_monomial
eval₂_eq_sum_range' 📖	mathematical	natDegree	eval₂ Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.range Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe RingHom RingHom.instFunLike coeff Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	eval₂_eq_sum sum_over_range' RingHom.map_zero MulZeroClass.zero_mul
isUnit_of_isUnit_leadingCoeff_of_isUnit_map 📖	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero leadingCoeff Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semiring map	—	—	degree_eq_zero_of_isUnit IsDomain.to_noZeroDivisors IsDomain.toNontrivial eq_C_of_degree_eq_zero degree_map_eq_of_leadingCoeff_ne_zero IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass NeZero.one degree_eq_iff_natDegree_eq map_zero nontrivial
iterate_comp_eval 📖	mathematical	—	eval CommSemiring.toSemiring Nat.iterate Polynomial comp	—	iterate_comp_eval₂
iterate_comp_eval₂ 📖	mathematical	—	eval₂ CommSemiring.toSemiring Nat.iterate Polynomial comp	—	Function.iterate_succ_apply' eval₂_comp
leadingCoeff_map_of_leadingCoeff_ne_zero 📖	mathematical	—	leadingCoeff map DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	coeff_map natDegree_map_of_leadingCoeff_ne_zero
mapEquiv_apply 📖	mathematical	—	DFunLike.coe RingEquiv Polynomial instMul instAdd EquivLike.toFunLike RingEquiv.instEquivLike mapEquiv map RingHomClass.toRingHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd	—	—
mapEquiv_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv Polynomial instMul instAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm mapEquiv map RingHomClass.toRingHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd	—	—
map_monic_eq_zero_iff 📖	mathematical	Monic	map Polynomial instZero DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	Monic.leadingCoeff RingHom.map_one mul_one coeff_map MulZeroClass.mul_zero ext
map_monic_ne_zero 📖	—	Monic	—	—	RingHom.map_one_ne_zero map_monic_eq_zero_iff
natDegree_map_le 📖	mathematical	—	natDegree map	—	natDegree_le_natDegree degree_map_le
natDegree_map_lt 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike leadingCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	natDegree map	—	natDegree_lt_natDegree degree_map_lt map_zero
natDegree_map_lt' 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike leadingCoeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring natDegree	map	—	natDegree_zero natDegree_map_lt
natDegree_map_of_leadingCoeff_ne_zero 📖	mathematical	—	natDegree map	—	natDegree_eq_of_degree_eq degree_map_eq_of_leadingCoeff_ne_zero
nextCoeff_map_of_leadingCoeff_ne_zero 📖	mathematical	—	nextCoeff map DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	—

---

← Back to Index