Lemmas

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

Statistics

Metric	Count
Definitions	0
Theorems coe_lt_degree, coeff_add_eq_left_of_lt, coeff_add_eq_right_of_lt, coeff_pow_eq_ite_of_natDegree_le_of_le, coeff_pow_of_natDegree_le, coeff_sub_eq_left_of_lt, coeff_sub_eq_neg_right_of_lt, comp_eq_zero_iff, comp_neg_X_eq_zero_iff, comp_neg_X_leadingCoeff_eq, degree_C_mul, degree_C_mul_of_mul_ne_zero, degree_add_degree_leadingCoeff_inv, degree_comp, degree_comp_neg_X, degree_leadingCoeff_inv, degree_map_eq_iff, degree_map_eq_of_injective, degree_map_eq_of_isUnit_leadingCoeff, degree_mul_C, degree_mul_leadingCoeff_inv, degree_mul_leadingCoeff_self_inv, degree_pos_of_eval₂_root, degree_pos_of_root, degree_sum_eq_of_disjoint, dvd_mul_leadingCoeff_inv, eq_natDegree_of_le_mem_support, irreducible_mul_leadingCoeff_inv, leadingCoeff_comp, leadingCoeff_map_eq_of_isUnit_leadingCoeff, leadingCoeff_map_of_injective, monic_mul_leadingCoeff_inv, natDegree_C_mul, natDegree_C_mul_eq_of_mul_eq_one, natDegree_C_mul_le, natDegree_C_mul_of_mul_ne_zero, natDegree_add_coeff_mul, natDegree_add_le_iff_left, natDegree_add_le_iff_right, natDegree_comp, natDegree_comp_eq_of_mul_ne_zero, natDegree_comp_le, natDegree_eq_one, natDegree_iterate_comp, natDegree_le_iff_coeff_eq_zero, natDegree_lt_coeff_mul, natDegree_map_eq_iff, natDegree_map_eq_of_injective, natDegree_map_eq_of_isUnit_leadingCoeff, natDegree_mul_C, natDegree_mul_C_eq_of_mul_eq_one, natDegree_mul_C_eq_of_mul_ne_zero, natDegree_mul_C_le, natDegree_mul_leadingCoeff_inv, natDegree_mul_leadingCoeff_self_inv, natDegree_pos_of_eval₂_root, natDegree_pos_of_nextCoeff_ne_zero, natDegree_sub, natDegree_sub_le_iff_left, natDegree_sub_le_iff_right, natDegree_sum_eq_of_disjoint, nextCoeff_C_mul, nextCoeff_C_mul_X_add_C, nextCoeff_map, nextCoeff_map_eq_of_isUnit_leadingCoeff, nextCoeff_mul_C, subsingleton_isRoot_of_natDegree_eq_one	67
Total	67

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_lt_degree 📖	mathematical	—	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne degree natDegree	—	Nat.instCanonicallyOrderedAdd degree_eq_natDegree WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithBot.zeroLEOneClass Nat.instZeroLEOneClass WithBot.charZero Nat.instCharZero
coeff_add_eq_left_of_lt 📖	mathematical	natDegree	coeff Polynomial instAdd	—	coeff_add coeff_eq_zero_of_natDegree_lt add_zero
coeff_add_eq_right_of_lt 📖	mathematical	natDegree	coeff Polynomial instAdd	—	add_comm coeff_add_eq_left_of_lt
coeff_pow_eq_ite_of_natDegree_le_of_le 📖	mathematical	natDegree	coeff Polynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	eq_or_ne coeff_pow_of_natDegree_le coeff_eq_zero_of_natDegree_lt lt_of_le_of_lt natDegree_pow_le_of_le lt_of_le_of_ne
coeff_pow_of_natDegree_le 📖	mathematical	natDegree	coeff Polynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	pow_zero MulZeroClass.zero_mul coeff_one_zero pow_succ coeff_mul_add_eq_of_natDegree_le LE.le.trans natDegree_pow_le le_trans mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing le_refl
coeff_sub_eq_left_of_lt 📖	mathematical	natDegree Ring.toSemiring	coeff Polynomial instSub	—	sub_eq_add_neg coeff_add_eq_left_of_lt natDegree_neg
coeff_sub_eq_neg_right_of_lt 📖	mathematical	natDegree Ring.toSemiring	coeff Polynomial instSub NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	sub_eq_add_neg coeff_add_eq_right_of_lt coeff_neg
comp_eq_zero_iff 📖	mathematical	—	comp Polynomial instZero eval coeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe RingHom semiring RingHom.instFunLike C	—	mul_eq_zero IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd natDegree_comp natDegree_zero eq_C_of_natDegree_eq_zero C_comp C_eq_zero comp_C zero_comp C_0
comp_neg_X_eq_zero_iff 📖	mathematical	—	comp Ring.toSemiring Polynomial instNeg X instZero	—	comp_neg_X_leadingCoeff_eq
comp_neg_X_leadingCoeff_eq 📖	mathematical	—	leadingCoeff Ring.toSemiring comp Polynomial instNeg X Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne natDegree	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Monic.leadingCoeff natDegree_of_subsingleton pow_zero mul_one zero_comp MulZeroClass.mul_zero leadingCoeff.eq_1 natDegree_comp_eq_of_mul_ne_zero leadingCoeff_neg coeff_comp_degree_mul_degree natDegree_neg natDegree_X Commute.eq Commute.pow_left Commute.neg_one_left
degree_C_mul 📖	mathematical	—	degree Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	degree_mul degree_C zero_add
degree_C_mul_of_mul_ne_zero 📖	mathematical	—	degree Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	degree_mul' leadingCoeff_C degree_C left_ne_zero_of_mul zero_add
degree_add_degree_leadingCoeff_inv 📖	mathematical	—	WithBot WithBot.add degree DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring DFunLike.coe RingHom Polynomial Semiring.toNonAssocSemiring semiring RingHom.instFunLike C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero leadingCoeff	—	degree_mul IsDomain.to_noZeroDivisors DivisionRing.isDomain degree_mul_leadingCoeff_self_inv
degree_comp 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree	comp Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring WithBot.instCommSemiring Nat.instCommSemiring Nat.instPartialOrder Nat.instCanonicallyOrderedAdd IsStrictOrderedRing.noZeroDivisors Nat.instLinearOrder Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Distrib.toAdd Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Nat.instNontrivial	—	Nat.instCanonicallyOrderedAdd IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instNontrivial eq_or_ne zero_comp degree_zero WithBot.bot_mul' LT.lt.ne' degree_eq_natDegree ne_zero_of_degree_gt Nat.cast_mul natDegree_comp
degree_comp_neg_X 📖	mathematical	—	degree Ring.toSemiring comp Polynomial instNeg X	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim degree_of_subsingleton eq_or_ne zero_comp degree_eq_natDegree WithBot.charZero Nat.instCharZero natDegree_comp_eq_of_mul_ne_zero leadingCoeff_neg Monic.leadingCoeff natDegree_neg natDegree_X mul_one
degree_leadingCoeff_inv 📖	mathematical	—	degree DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring DFunLike.coe RingHom Polynomial Semiring.toNonAssocSemiring semiring RingHom.instFunLike C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero leadingCoeff WithBot WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass	—	degree_C
degree_map_eq_iff 📖	mathematical	—	degree map Polynomial instZero	—	eq_or_ne map_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass degree_eq_bot coeff_natDegree coeff_map leadingCoeff_eq_zero degree_map_eq_of_leadingCoeff_ne_zero
degree_map_eq_of_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	degree map	—	MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
degree_map_eq_of_isUnit_leadingCoeff 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero leadingCoeff	degree map	—	degree_map_eq_of_leadingCoeff_ne_zero IsUnit.ne_zero RingHom.isUnit_map
degree_mul_C 📖	mathematical	—	degree Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	degree_mul degree_C add_zero
degree_mul_leadingCoeff_inv 📖	mathematical	—	degree DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero leadingCoeff	—	inv_ne_zero leadingCoeff_eq_zero degree_mul_C IsDomain.to_noZeroDivisors DivisionRing.isDomain
degree_mul_leadingCoeff_self_inv 📖	mathematical	—	degree DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero leadingCoeff	—	inv_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.mul_zero degree_mul_leadingCoeff_inv
degree_pos_of_eval₂_root 📖	mathematical	eval₂ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero Nat.instMulZeroClass degree	—	natDegree_pos_iff_degree_pos natDegree_pos_of_eval₂_root
degree_pos_of_root 📖	mathematical	IsRoot	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree	—	lt_of_not_ge eq_C_of_degree_le_zero eval_C IsRoot.eq_1 map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
degree_sum_eq_of_disjoint 📖	mathematical	Set.Pairwise setOf Finset Finset.instMembership Polynomial instZero Function.onFun WithBot degree	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring Finset.sup WithBot.semilatticeSup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeNat WithBot.instOrderBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	Finset.induction_on Finset.sup_empty Finset.sum_insert Finset.sup_insert lt_trichotomy Set.Pairwise.mono sup_eq_right LT.lt.le degree_add_eq_right_of_degree_lt Finset.eq_empty_or_nonempty add_zero sup_of_le_left Finset.exists_mem_eq_sup zero_add sup_of_le_right Mathlib.Tactic.Contrapose.contrapose₃ sup_eq_left degree_add_eq_left_of_degree_lt
dvd_mul_leadingCoeff_inv 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero Semiring.toNonUnitalSemiring semiring instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero leadingCoeff	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass instIsLocalHomOfMonoidWithZeroHomClassOfNontrivial nontrivial DivisionRing.toNontrivial
eq_natDegree_of_le_mem_support 📖	—	natDegree Finset Finset.instMembership support	—	—	le_antisymm le_natDegree_of_mem_supp
irreducible_mul_leadingCoeff_inv 📖	mathematical	—	Irreducible Polynomial DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero leadingCoeff	—	inv_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.mul_zero irreducible_mul_isUnit isUnit_C inv_ne_zero leadingCoeff_ne_zero
leadingCoeff_comp 📖	mathematical	—	leadingCoeff comp Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero natDegree	—	coeff_comp_degree_mul_degree natDegree_comp coeff_natDegree
leadingCoeff_map_eq_of_isUnit_leadingCoeff 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero leadingCoeff	map DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	leadingCoeff_map_of_leadingCoeff_ne_zero IsUnit.ne_zero RingHom.isUnit_map
leadingCoeff_map_of_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	leadingCoeff map	—	natDegree_map_eq_of_injective coeff_map
monic_mul_leadingCoeff_inv 📖	mathematical	—	Monic DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero leadingCoeff	—	Monic.eq_1 leadingCoeff_mul IsDomain.to_noZeroDivisors DivisionRing.isDomain leadingCoeff_C mul_inv_cancel₀ leadingCoeff_eq_zero
natDegree_C_mul 📖	mathematical	—	natDegree Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	degree_C_mul
natDegree_C_mul_eq_of_mul_eq_one 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	natDegree Polynomial instMul DFunLike.coe RingHom semiring RingHom.instFunLike C	—	le_antisymm natDegree_C_mul_le one_mul C_1 map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mul_assoc
natDegree_C_mul_le 📖	mathematical	—	natDegree Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	natDegree_C zero_add natDegree_mul_le
natDegree_C_mul_of_mul_ne_zero 📖	mathematical	—	natDegree Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	eq_natDegree_of_le_mem_support natDegree_C_mul_le mem_support_iff coeff_C_mul
natDegree_add_coeff_mul 📖	mathematical	—	coeff Polynomial instMul natDegree Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	coeff_mul_degree_add_degree
natDegree_add_le_iff_left 📖	mathematical	natDegree	Polynomial instAdd	—	natDegree_le_iff_coeff_eq_zero coeff_add add_zero natDegree_add_le_of_degree_le
natDegree_add_le_iff_right 📖	mathematical	natDegree	Polynomial instAdd	—	add_comm natDegree_add_le_iff_left
natDegree_comp 📖	mathematical	—	natDegree comp	—	degree_le_zero_iff natDegree_eq_zero_iff_degree_le_zero comp_C natDegree_C MulZeroClass.mul_zero zero_comp MulZeroClass.zero_mul natDegree_comp_eq_of_mul_ne_zero isReduced_of_noZeroDivisors ne_zero_of_natDegree_gt
natDegree_comp_eq_of_mul_ne_zero 📖	mathematical	—	natDegree comp	—	le_antisymm natDegree_comp_le MulZeroClass.mul_zero Nat.instCanonicallyOrderedAdd natDegree_eq_of_le_of_coeff_ne_zero coeff_comp_degree_mul_degree
natDegree_comp_le 📖	mathematical	—	natDegree comp	—	natDegree_zero WithBot.coe_le_coe degree_eq_natDegree comp_eq_sum_left degree_sum_le Finset.sup_le degree_mul_le add_le_add WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithBot.addRightMono covariant_swap_add_of_covariant_add degree_le_natDegree degree_pow_le le_imp_le_of_le_of_le add_le_add_right nsmul_le_nsmul_right le_refl natDegree_C Nat.cast_zero zero_add Nat.instCanonicallyOrderedAdd IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instNontrivial nsmul_eq_mul Nat.cast_mul mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono IsStrictOrderedRing.toIsOrderedRing le_natDegree_of_ne_zero mem_support_iff
natDegree_eq_one 📖	mathematical	—	natDegree Polynomial instAdd instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C X	—	leadingCoeff_eq_zero coeff_natDegree ext coeff_add mul_coeff_zero coeff_C_zero coeff_X_zero MulZeroClass.mul_zero zero_add coeff_mul_X coeff_C_succ add_zero coeff_eq_zero_of_natDegree_lt IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.instNoMaxOrder Nat.instCanonicallyOrderedAdd natDegree_add_C natDegree_C_mul_X
natDegree_iterate_comp 📖	mathematical	—	natDegree Nat.iterate Polynomial comp Monoid.toNatPow Nat.instMonoid	—	pow_zero one_mul Function.iterate_succ_apply' natDegree_comp pow_succ' mul_assoc
natDegree_le_iff_coeff_eq_zero 📖	mathematical	—	natDegree coeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithBot.zeroLEOneClass Nat.instZeroLEOneClass WithBot.charZero Nat.instCharZero
natDegree_lt_coeff_mul 📖	mathematical	natDegree	coeff Polynomial instMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	coeff_eq_zero_of_natDegree_lt LE.le.trans_lt natDegree_mul_le
natDegree_map_eq_iff 📖	mathematical	—	natDegree map	—	eq_or_ne
natDegree_map_eq_of_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	natDegree map	—	natDegree_eq_of_degree_eq degree_map_eq_of_injective
natDegree_map_eq_of_isUnit_leadingCoeff 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero leadingCoeff	natDegree map	—	natDegree_eq_natDegree degree_map_eq_of_isUnit_leadingCoeff
natDegree_mul_C 📖	mathematical	—	natDegree Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	degree_mul_C
natDegree_mul_C_eq_of_mul_eq_one 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	natDegree Polynomial instMul DFunLike.coe RingHom semiring RingHom.instFunLike C	—	le_antisymm natDegree_mul_C_le mul_one C_1 map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mul_assoc
natDegree_mul_C_eq_of_mul_ne_zero 📖	mathematical	—	natDegree Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	eq_natDegree_of_le_mem_support natDegree_mul_C_le mem_support_iff coeff_mul_C
natDegree_mul_C_le 📖	mathematical	—	natDegree Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	natDegree_C add_zero natDegree_mul_le
natDegree_mul_leadingCoeff_inv 📖	mathematical	—	natDegree DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero leadingCoeff	—	natDegree_eq_of_degree_eq degree_mul_leadingCoeff_inv
natDegree_mul_leadingCoeff_self_inv 📖	mathematical	—	natDegree DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero leadingCoeff	—	natDegree_eq_of_degree_eq degree_mul_leadingCoeff_self_inv
natDegree_pos_of_eval₂_root 📖	mathematical	eval₂ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	natDegree	—	lt_of_not_ge eq_C_of_natDegree_le_zero eval₂_C map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
natDegree_pos_of_nextCoeff_ne_zero 📖	mathematical	—	natDegree	—	—
natDegree_sub 📖	mathematical	—	natDegree Ring.toSemiring Polynomial instSub	—	natDegree_neg neg_sub
natDegree_sub_le_iff_left 📖	mathematical	natDegree Ring.toSemiring	Polynomial instSub	—	sub_eq_add_neg natDegree_add_le_iff_left natDegree_neg
natDegree_sub_le_iff_right 📖	mathematical	natDegree Ring.toSemiring	Polynomial instSub	—	natDegree_sub natDegree_sub_le_iff_left
natDegree_sum_eq_of_disjoint 📖	mathematical	Set.Pairwise setOf Finset Finset.instMembership Polynomial instZero Function.onFun natDegree	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring Finset.sup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeNat Nat.instOrderBot	—	natDegree_eq_of_degree_eq_some degree_sum_eq_of_disjoint Set.Pairwise.imp natDegree_eq_of_degree_eq Finset.sup'_eq_sup Nat.cast_withBot Finset.coe_sup' le_antisymm Finset.sup'_le_iff Finset.sup'_congr degree_eq_natDegree Finset.le_sup' Mathlib.Tactic.Contrapose.contrapose₂ Eq.ge Finset.sum_eq_zero Mathlib.Tactic.Push.not_and_eq natDegree_zero Finset.sup_eq_bot_iff
nextCoeff_C_mul 📖	mathematical	—	nextCoeff Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.zero_mul mul_ite MulZeroClass.mul_zero natDegree_C_mul coeff_C_mul
nextCoeff_C_mul_X_add_C 📖	mathematical	—	nextCoeff Polynomial instAdd instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C X	—	nextCoeff_of_natDegree_pos natDegree_add_C natDegree_C_mul_X Nat.instZeroLEOneClass tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub coeff_add mul_coeff_zero coeff_C_zero coeff_X_zero MulZeroClass.mul_zero zero_add
nextCoeff_map 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	nextCoeff map	—	natDegree_map_eq_of_injective map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass coeff_map
nextCoeff_map_eq_of_isUnit_leadingCoeff 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero leadingCoeff	nextCoeff map DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	nextCoeff_map_of_leadingCoeff_ne_zero IsUnit.ne_zero RingHom.isUnit_map
nextCoeff_mul_C 📖	mathematical	—	nextCoeff Polynomial instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.mul_zero natDegree_mul_C coeff_mul_C ite_mul MulZeroClass.zero_mul
subsingleton_isRoot_of_natDegree_eq_one 📖	mathematical	natDegree	Set.Subsingleton setOf IsRoot	—	natDegree_eq_one mul_left_cancel₀

---

← Back to Index