MonomialOrder

📁 Source: Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

Statistics

Metric	Count
Definitions `MonomialOrder`, `decidable`, `degree`, `leadingCoeff`, `leadingTerm`, `sPolynomial`	6
Theorems `C_mul_leadingCoeff_monomial_degree`, `add_of_lt`, `coeff_degree`, `leadingCoeff_eq_one`, `mul`, `ne_zero`, `of_subsingleton`, `pow`, `prod`, `coeff_degree_eq_zero_iff`, `coeff_degree_ne_zero_iff`, `coeff_eq_zero_of_lt`, `coeff_mul_of_add_of_degree_le`, `coeff_mul_of_degree_add`, `coeff_pow_nsmul_degree`, `coeff_prod_sum_degree`, `coeff_sPolynomial_sup_eq_zero`, `degree_C`, `degree_X`, `degree_X_add_C`, `degree_X_le_single`, `degree_X_sub_C`, `degree_add_eq_right_of_lt`, `degree_add_le`, `degree_add_of_lt`, `degree_add_of_ne`, `degree_eq_zero_iff`, `degree_eq_zero_iff_totalDegree_eq_zero`, `degree_le_iff`, `degree_leadingTerm`, `degree_leadingTerm_mul`, `degree_lt_iff`, `degree_lt_of_left_ne_zero_of_degree_mul_lt`, `degree_mem_support`, `degree_mem_support_iff`, `degree_monomial`, `degree_monomial_le`, `degree_mul`, `degree_mul'`, `degree_mul_le`, `degree_mul_leadingTerm`, `degree_mul_lt_iff_left_lt_of_ne_zero`, `degree_mul_of_isRegular_left`, `degree_mul_of_isRegular_right`, `degree_mul_of_left_mem_nonZeroDivisors`, `degree_mul_of_mul_leadingCoeff_ne_zero`, `degree_mul_of_right_mem_nonZeroDivisors`, `degree_ne_zero_of_sub_leadingTerm_ne_zero`, `degree_neg`, `degree_one`, `degree_pow`, `degree_pow_le`, `degree_pow_of_pow_leadingCoeff_ne_zero`, `degree_prod`, `degree_prod_le`, `degree_prod_of_mem_nonZeroDivisors`, `degree_prod_of_regular`, `degree_sPolynomial`, `degree_sPolynomial_le`, `degree_sPolynomial_lt_sup_degree`, `degree_smul`, `degree_smul_le`, `degree_smul_of_isRegular`, `degree_smul_of_mem_nonZeroDivisors`, `degree_sub_le`, `degree_sub_leadingTerm_le`, `degree_sub_leadingTerm_lt_degree`, `degree_sub_leadingTerm_lt_iff`, `degree_sub_of_lt`, `degree_subsingleton`, `degree_sum_le`, `degree_zero`, `eq_C_of_degree_eq_zero`, `image_leadingTerm_insert_zero`, `image_leadingTerm_sdiff_singleton_zero`, `isUnit_leadingCoeff`, `le_degree`, `leadingCoeff_C`, `leadingCoeff_X`, `leadingCoeff_add_of_lt`, `leadingCoeff_eq_zero_iff`, `leadingCoeff_leadingTerm`, `leadingCoeff_monomial`, `leadingCoeff_mul`, `leadingCoeff_mul_of_isRegular_left`, `leadingCoeff_mul_of_isRegular_right`, `leadingCoeff_mul_of_left_mem_nonZeroDivisors`, `leadingCoeff_mul_of_mul_leadingCoeff_ne_zero`, `leadingCoeff_mul_of_right_mem_nonZeroDivisors`, `leadingCoeff_ne_zero_iff`, `leadingCoeff_neg`, `leadingCoeff_one`, `leadingCoeff_pow`, `leadingCoeff_pow_of_pow_leadingCoeff_ne_zero`, `leadingCoeff_prod_of_mem_nonZeroDivisors`, `leadingCoeff_prod_of_regular`, `leadingCoeff_sub_of_lt`, `leadingCoeff_zero`, `leadingTerm_C`, `leadingTerm_eq_zero_iff`, `leadingTerm_leadingTerm`, `leadingTerm_monomial`, `leadingTerm_zero`, `monic_X`, `monic_X_add_C`, `monic_X_sub_C`, `monic_monomial`, `monic_monomial_one`, `monic_one`, `ne_zero_of_degree_ne_zero`, `notMem_support_of_degree_lt`, `sPolynomial_antisymm`, `sPolynomial_decomposition`, `sPolynomial_decomposition'`, `sPolynomial_def`, `sPolynomial_leadingTerm_mul`, `sPolynomial_leadingTerm_mul'`, `sPolynomial_left_zero`, `sPolynomial_lt_of_degree_ne_zero_of_degree_eq`, `sPolynomial_monomial_mul`, `sPolynomial_monomial_mul'`, `sPolynomial_mul_monomial`, `sPolynomial_right_zero`, `sPolynomial_self`	124
Total	130

MonomialOrder

Definitions

Name	Category	Theorems
`degree` 📖	CompOp	73 math math: `sPolynomial_leadingTerm_mul'`, `degree_add_of_ne`, `degree_monomial`, `degree_X`, `degree_sub_le`, `degree_lt_iff`, `degree_mem_support_iff`, `div_single`, `degree_add_le`, `le_degree`, `degree_mul_leadingTerm`, `span_leadingTerm_eq_span_monomial`, `span_leadingTerm_eq_span_monomial₀`, `degree_neg`, `coeff_prod_sum_degree`, `degree_le_iff`, `degree_mul_of_isRegular_right`, `MvPolynomial.degree_degLexDegree`, `degree_sum_le`, `degree_mul_of_mul_leadingCoeff_ne_zero`, `degree_subsingleton`, `degree_leadingTerm_mul`, `span_leadingTerm_eq_span_monomial'`, `degree_X_sub_C`, `degree_mul_lt_iff_left_lt_of_ne_zero`, `degree_smul_le`, `degree_mul_le`, `sPolynomial_def`, `degree_mul_of_left_mem_nonZeroDivisors`, `degree_pow_le`, `degree_C`, `coeff_degree_eq_zero_iff`, `degree_smul_of_isRegular`, `degree_one`, `sPolynomial_monomial_mul`, `degree_eq_zero_iff_totalDegree_eq_zero`, `degree_eq_zero_iff`, `degree_mem_support`, `degree_prod_le`, `div_set`, `degree_zero`, `coeff_pow_nsmul_degree`, `degree_pow`, `sPolynomial_monomial_mul'`, `Monic.coeff_degree`, `degree_prod`, `degree_smul`, `degree_leadingTerm`, `degree_mul_of_isRegular_left`, `div`, `degree_sPolynomial_le`, `degree_X_add_C`, `coeff_mul_of_degree_add`, `degree_sub_leadingTerm_lt_degree`, `coeff_sPolynomial_sup_eq_zero`, `degree_mul`, `degree_monomial_le`, `degree_sub_LTerm_lt`, `degree_prod_of_regular`, `C_mul_leadingCoeff_monomial_degree`, `degree_mul'`, `degree_sPolynomial_lt_sup_degree`, `degree_sub_leadingTerm_lt_iff`, `degree_mul_of_right_mem_nonZeroDivisors`, `degree_sub_leadingTerm_le`, `degree_smul_of_mem_nonZeroDivisors`, `degree_sub_LTerm_le`, `sPolynomial_mul_monomial`, `degree_prod_of_mem_nonZeroDivisors`, `degree_pow_of_pow_leadingCoeff_ne_zero`, `sPolynomial_leadingTerm_mul`, `degree_sPolynomial`, `degree_X_le_single`
`leadingCoeff` 📖	CompOp	25 math math: `sPolynomial_leadingTerm_mul'`, `leadingCoeff_eq_zero_iff`, `leadingCoeff_mul`, `eq_C_of_degree_eq_zero`, `isUnit_leadingCoeff`, `coeff_prod_sum_degree`, `leadingCoeff_pow_of_pow_leadingCoeff_ne_zero`, `leadingCoeff_leadingTerm`, `sPolynomial_def`, `leadingCoeff_monomial`, `Monic.leadingCoeff_eq_one`, `leadingCoeff_add_of_lt`, `degree_eq_zero_iff`, `leadingCoeff_neg`, `leadingCoeff_C`, `coeff_pow_nsmul_degree`, `leadingCoeff_pow`, `leadingCoeff_zero`, `leadingCoeff_X`, `leadingCoeff_sub_of_lt`, `coeff_mul_of_degree_add`, `leadingCoeff_one`, `C_mul_leadingCoeff_monomial_degree`, `leadingCoeff_mul_of_mul_leadingCoeff_ne_zero`, `sPolynomial_leadingTerm_mul`
`leadingTerm` 📖	CompOp	22 math math: `sPolynomial_leadingTerm_mul'`, `span_leadingTerm_sdiff_singleton_zero`, `leadingTerm_zero`, `image_leadingTerm_sdiff_singleton_zero`, `leadingTerm_monomial`, `degree_mul_leadingTerm`, `span_leadingTerm_eq_span_monomial`, `span_leadingTerm_eq_span_monomial₀`, `degree_leadingTerm_mul`, `span_leadingTerm_eq_span_monomial'`, `leadingCoeff_leadingTerm`, `leadingTerm_leadingTerm`, `image_leadingTerm_insert_zero`, `leadingTerm_C`, `span_leadingTerm_insert_zero`, `degree_leadingTerm`, `degree_sub_leadingTerm_lt_degree`, `C_mul_leadingCoeff_monomial_degree`, `leadingTerm_eq_zero_iff`, `degree_sub_leadingTerm_lt_iff`, `degree_sub_leadingTerm_le`, `sPolynomial_leadingTerm_mul`
`sPolynomial` 📖	CompOp	19 math math: `sPolynomial_leadingTerm_mul'`, `sPolynomial_self`, `sPolynomial_def`, `sPolynomial_antisymm`, `sPolynomial_left_zero`, `sPolynomial_decomposition`, `sPolynomial_right_zero`, `sPolynomial_monomial_mul`, `sPolynomial_monomial_mul'`, `sPolynomial_mem_ideal`, `degree_sPolynomial_le`, `coeff_sPolynomial_sup_eq_zero`, `sPolynomial_mem_sup_ideal`, `sPolynomial_lt_of_degree_ne_zero_of_degree_eq`, `sPolynomial_decomposition'`, `degree_sPolynomial_lt_sup_degree`, `sPolynomial_mul_monomial`, `sPolynomial_leadingTerm_mul`, `degree_sPolynomial`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C_mul_leadingCoeff_monomial_degree` 📖	mathematical	—	`MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `MvPolynomial.C` `leadingCoeff` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `MvPolynomial.module` `LinearMap.instFunLike` `MvPolynomial.monomial` `degree` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `leadingTerm`	—	`MvPolynomial.C_mul_monomial` `mul_one` `leadingTerm.eq_1`
`coeff_degree_eq_zero_iff` 📖	mathematical	—	`MvPolynomial.coeff` `degree` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial` `MvPolynomial.commSemiring`	—	`leadingCoeff_eq_zero_iff`
`coeff_degree_ne_zero_iff` 📖	—	—	—	—	`leadingCoeff_ne_zero_iff`
`coeff_eq_zero_of_lt` 📖	mathematical	`syn` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree`	`MvPolynomial.coeff` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`not_le` `le_degree` `MvPolynomial.mem_support_iff`
`coeff_mul_of_add_of_degree_le` 📖	mathematical	`syn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree`	`MvPolynomial.coeff` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`MvPolynomial.coeff_mul` `Finset.sum_eq_single` `coeff_eq_zero_of_lt` `MulZeroClass.zero_mul` `not_le` `AddEquiv.injective` `le_antisymm` `le_trans` `not_lt` `le_of_add_le_add_right` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `iocam` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `map_add` `AddMonoidHomClass.toAddHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `IsCancelAdd.toIsLeftCancelAdd` `Finsupp.instIsLeftCancelAdd` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `MulZeroClass.mul_zero` `instIsEmptyFalse`
`coeff_mul_of_degree_add` 📖	mathematical	—	`MvPolynomial.coeff` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `degree` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `leadingCoeff`	—	`coeff_mul_of_add_of_degree_le` `le_of_eq`
`coeff_pow_nsmul_degree` 📖	mathematical	—	`MvPolynomial.coeff` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instNatSMul` `Nat.instAddMonoid` `degree` `MvPolynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `leadingCoeff`	—	`zero_nsmul` `pow_zero` `MvPolynomial.coeff_zero_one` `add_smul` `one_smul` `pow_add` `pow_one` `coeff_mul_of_add_of_degree_le` `degree_pow_le` `le_rfl` `leadingCoeff.eq_1`
`coeff_prod_sum_degree` 📖	mathematical	—	`MvPolynomial.coeff` `Finset.sum` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `degree` `Finset.prod` `MvPolynomial` `CommSemiring.toCommMonoid` `MvPolynomial.commSemiring` `leadingCoeff`	—	`Finset.induction_on` `MvPolynomial.coeff_zero_one` `Finset.sum_insert` `Finset.prod_insert` `coeff_mul_of_add_of_degree_le` `le_of_eq` `degree_prod_le`
`coeff_sPolynomial_sup_eq_zero` 📖	mathematical	—	`MvPolynomial.coeff` `CommRing.toCommSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `SemilatticeSup.toMax` `Finsupp.semilatticeSup` `Lattice.toSemilatticeSup` `Nat.instLattice` `degree` `sPolynomial` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `sPolynomial_def` `MvPolynomial.coeff_sub` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Finsupp.instCanonicallyOrderedAddOfAddLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finsupp.isOrderedAddMonoid` `Finsupp.orderedSub` `le_sup_left` `MvPolynomial.coeff_monomial_mul` `le_sup_right` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero`
`degree_C` 📖	mathematical	—	`degree` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.C` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instZero`	—	`degree_eq_zero_iff_totalDegree_eq_zero` `MvPolynomial.totalDegree_C`
`degree_X` 📖	mathematical	—	`degree` `MvPolynomial.X` `Finsupp.single` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`degree_monomial` `one_ne_zero` `NeZero.one`
`degree_X_add_C` 📖	mathematical	—	`degree` `CommRing.toCommSemiring` `MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `MvPolynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.C` `Finsupp.single` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`degree_add_of_lt` `degree_C` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `degree_X` `bot_eq_zero` `bot_lt_iff_ne_bot` `EquivLike.toEmbeddingLike`
`degree_X_le_single` 📖	mathematical	—	`syn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `MvPolynomial.X` `Finsupp.single`	—	`degree_monomial_le`
`degree_X_sub_C` 📖	mathematical	—	`degree` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial` `MvPolynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.C` `Finsupp.single` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`sub_eq_add_neg` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `degree_X_add_C`
`degree_add_eq_right_of_lt` 📖	mathematical	`syn` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree`	`MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`add_comm` `degree_add_of_lt`
`degree_add_le` 📖	mathematical	—	`syn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`AddEquiv.apply_symm_apply` `degree_le_iff` `le_degree` `MvPolynomial.coeff_add` `zero_add`
`degree_add_of_lt` 📖	mathematical	`syn` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree`	`MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`AddEquiv.injective` `le_antisymm` `le_trans` `degree_add_le` `le_of_lt` `le_degree` `MvPolynomial.mem_support_iff` `MvPolynomial.coeff_add` `coeff_eq_zero_of_lt` `add_zero` `leadingCoeff.eq_1` `leadingCoeff_ne_zero_iff` `not_le` `degree_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `bot_le`
`degree_add_of_ne` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `syn` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo`	—	`degree_add_of_lt` `sup_of_le_left` `le_of_lt` `add_comm` `EmbeddingLike.apply_eq_iff_eq` `EquivLike.toEmbeddingLike` `le_iff_eq_or_lt` `not_lt` `right_eq_sup`
`degree_eq_zero_iff` 📖	mathematical	—	`degree` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instZero` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.C` `leadingCoeff`	—	`eq_C_of_degree_eq_zero` `degree_C`
`degree_eq_zero_iff_totalDegree_eq_zero` 📖	mathematical	—	`degree` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instZero` `MvPolynomial.totalDegree`	—	`AddEquiv.injective` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `bot_eq_zero` `eq_bot_iff` `AddEquiv.map_zero` `degree_le_iff` `MvPolynomial.totalDegree_eq_zero_iff` `EquivLike.toEmbeddingLike` `Finsupp.ext_iff`
`degree_le_iff` 📖	mathematical	—	`syn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree`	—	`AddEquiv.apply_symm_apply`
`degree_leadingTerm` 📖	mathematical	—	`degree` `leadingTerm`	—	`degree_monomial` `degree_zero`
`degree_leadingTerm_mul` 📖	mathematical	—	`degree` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `leadingTerm`	—	`degree_mul` `degree_monomial` `Mathlib.Tactic.Push.not_and_or_eq` `leadingTerm_zero` `MulZeroClass.zero_mul` `degree_zero` `MulZeroClass.mul_zero`
`degree_lt_iff` 📖	mathematical	`syn` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `Finsupp.instZero`	`degree`	—	`AddEquiv.apply_symm_apply` `Finset.sup_lt_iff` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`degree_lt_of_left_ne_zero_of_degree_mul_lt` 📖	—	`syn` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	—	`degree_mul` `map_add` `AddMonoidHomClass.toAddHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `iocam` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `lt_of_le_of_lt'` `degree_mul_le` `MulZeroClass.mul_zero` `degree_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass`
`degree_mem_support` 📖	mathematical	—	`Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finset` `Finset.instMembership` `MvPolynomial.support` `degree`	—	`MvPolynomial.mem_support_iff` `coeff_degree_ne_zero_iff`
`degree_mem_support_iff` 📖	mathematical	—	`Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finset` `Finset.instMembership` `MvPolynomial.support` `degree`	—	`MvPolynomial.mem_support_iff` `coeff_degree_ne_zero_iff`
`degree_monomial` 📖	mathematical	—	`degree` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPolynomial.commSemiring` `Semiring.toModule` `MvPolynomial.module` `LinearMap.instFunLike` `MvPolynomial.monomial` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `NonUnitalNonAssocSemiring.toMulZeroClass` `Finsupp.instZero`	—	`MvPolynomial.support_monomial` `Finset.sup_empty` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `Finset.sup_singleton` `AddEquiv.symm_apply_apply`
`degree_monomial_le` 📖	mathematical	—	`syn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPolynomial.commSemiring` `Semiring.toModule` `MvPolynomial.module` `LinearMap.instFunLike` `MvPolynomial.monomial`	—	`AddEquiv.apply_symm_apply` `le_trans` `Finset.sup_mono` `MvPolynomial.support_monomial_subset` `Finset.sup_singleton`
`degree_mul` 📖	mathematical	—	`degree` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	`degree_mul_of_mul_leadingCoeff_ne_zero`
`degree_mul'` 📖	mathematical	—	`degree` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	`degree_mul` `ne_zero_and_ne_zero_of_mul`
`degree_mul_le` 📖	mathematical	—	`syn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`degree_le_iff` `not_lt` `MvPolynomial.mem_support_iff` `not_imp_not` `MvPolynomial.coeff_mul` `Finset.sum_eq_zero` `coeff_eq_zero_of_lt` `MulZeroClass.zero_mul` `lt_of_add_lt_add_left` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `iocam` `map_add` `AddMonoidHomClass.toAddHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `lt_imp_lt_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `le_refl` `MulZeroClass.mul_zero`
`degree_mul_leadingTerm` 📖	mathematical	—	`degree` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `leadingTerm`	—	`degree_leadingTerm_mul` `mul_comm`
`degree_mul_lt_iff_left_lt_of_ne_zero` 📖	mathematical	—	`syn` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`degree_lt_of_left_ne_zero_of_degree_mul_lt` `degree_mul` `map_add` `AddMonoidHomClass.toAddHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `Mathlib.Tactic.Contrapose.contrapose₃` `degree_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `iocam` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le`
`degree_mul_of_isRegular_left` 📖	mathematical	`IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `leadingCoeff`	`degree` `MvPolynomial` `MvPolynomial.commSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	`degree_mul_of_mul_leadingCoeff_ne_zero`
`degree_mul_of_isRegular_right` 📖	mathematical	`IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `leadingCoeff`	`degree` `MvPolynomial` `MvPolynomial.commSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	`mul_comm` `degree_mul_of_isRegular_left` `add_comm`
`degree_mul_of_left_mem_nonZeroDivisors` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `leadingCoeff`	`degree` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPolynomial.commSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	`degree_mul_of_mul_leadingCoeff_ne_zero` `not_imp_not` `mem_nonZeroDivisors_iff`
`degree_mul_of_mul_leadingCoeff_ne_zero` 📖	mathematical	—	`degree` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	`AddEquiv.injective` `le_antisymm` `degree_mul_le` `le_degree` `MvPolynomial.mem_support_iff` `coeff_mul_of_degree_add`
`degree_mul_of_right_mem_nonZeroDivisors` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `leadingCoeff`	`degree` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPolynomial.commSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid`	—	`degree_mul_of_left_mem_nonZeroDivisors` `mul_comm` `add_comm`
`degree_ne_zero_of_sub_leadingTerm_ne_zero` 📖	—	—	—	—	`Mathlib.Tactic.Contrapose.contrapose₄` `degree_eq_zero_iff` `leadingTerm_C` `sub_eq_zero`
`degree_neg` 📖	mathematical	—	`degree` `CommRing.toCommSemiring` `MvPolynomial` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial`	—	`MvPolynomial.support_neg`
`degree_one` 📖	mathematical	—	`degree` `MvPolynomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instZero`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `degree_subsingleton` `MvPolynomial.one_def` `degree_monomial` `NeZero.one`
`degree_pow` 📖	mathematical	—	`degree` `MvPolynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instNatSMul` `Nat.instAddMonoid`	—	`degree_zero` `smul_zero` `pow_zero` `degree_one` `zero_pow` `degree_pow_of_pow_leadingCoeff_ne_zero` `pow_ne_zero` `leadingCoeff_ne_zero_iff`
`degree_pow_le` 📖	mathematical	—	`syn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `MvPolynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `Finsupp.instNatSMul`	—	`pow_zero` `degree_one` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `zero_nsmul` `pow_add` `pow_one` `add_smul` `one_smul` `le_trans` `degree_mul_le` `map_add` `AddMonoidHomClass.toAddHomClass` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `iocam` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le`
`degree_pow_of_pow_leadingCoeff_ne_zero` 📖	mathematical	—	`degree` `MvPolynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instNatSMul` `Nat.instAddMonoid`	—	`AddEquiv.injective` `le_antisymm` `degree_pow_le` `le_degree` `MvPolynomial.mem_support_iff` `coeff_pow_nsmul_degree`
`degree_prod` 📖	mathematical	—	`degree` `Finset.prod` `MvPolynomial` `CommSemiring.toCommMonoid` `MvPolynomial.commSemiring` `Finset.sum` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid`	—	`subsingleton_or_nontrivial` `Finset.prod_congr` `Unique.instSubsingleton` `degree_subsingleton` `Finset.sum_congr` `Finset.sum_const_zero` `AddEquiv.injective` `le_antisymm` `degree_prod_le` `le_degree` `coeff_prod_sum_degree`
`degree_prod_le` 📖	mathematical	—	`syn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `Finset.prod` `MvPolynomial` `CommSemiring.toCommMonoid` `MvPolynomial.commSemiring` `Finset.sum` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid`	—	`Finset.induction_on` `MvPolynomial.C_1` `degree_C` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `le_refl` `Finset.prod_insert` `Finset.sum_insert` `le_trans` `degree_mul_le` `map_add` `AddMonoidHomClass.toAddHomClass` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `iocam` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `contravariant_lt_of_covariant_le`
`degree_prod_of_mem_nonZeroDivisors` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `leadingCoeff`	`degree` `Finset.prod` `MvPolynomial` `CommSemiring.toCommMonoid` `MvPolynomial.commSemiring` `Finset.sum` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid`	—	`subsingleton_or_nontrivial` `Finset.prod_congr` `Unique.instSubsingleton` `degree_subsingleton` `Finset.sum_congr` `Finset.sum_const_zero` `AddEquiv.injective` `le_antisymm` `degree_prod_le` `le_degree` `MvPolynomial.mem_support_iff` `coeff_prod_sum_degree` `nonZeroDivisors.ne_zero` `prod_mem_nonZeroDivisors_of_mem_nonZeroDivisors`
`degree_prod_of_regular` 📖	mathematical	`IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `leadingCoeff`	`degree` `Finset.prod` `MvPolynomial` `CommSemiring.toCommMonoid` `MvPolynomial.commSemiring` `Finset.sum` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid`	—	`subsingleton_or_nontrivial` `Finset.prod_congr` `Unique.instSubsingleton` `degree_subsingleton` `Finset.sum_congr` `Finset.sum_const_zero` `AddEquiv.injective` `le_antisymm` `degree_prod_le` `le_degree` `MvPolynomial.mem_support_iff` `coeff_prod_sum_degree` `IsRegular.ne_zero` `IsRegular.prod`
`degree_sPolynomial` 📖	mathematical	—	`syn` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `CommRing.toCommSemiring` `sPolynomial` `SemilatticeSup.toMax` `Finsupp.semilatticeSup` `Lattice.toSemilatticeSup` `Nat.instLattice` `MvPolynomial` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial`	—	`degree_eq_zero_iff` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `sPolynomial_def` `sup_of_le_left` `tsub_self` `Finsupp.instCanonicallyOrderedAddOfAddLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finsupp.orderedSub` `LE.le.lt_of_ne` `degree_sPolynomial_le` `AddEquiv.injective` `Mathlib.Tactic.Contrapose.contrapose₄` `coeff_degree_eq_zero_iff` `coeff_sPolynomial_sup_eq_zero`
`degree_sPolynomial_le` 📖	mathematical	—	`syn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `CommRing.toCommSemiring` `sPolynomial` `SemilatticeSup.toMax` `Finsupp.semilatticeSup` `Lattice.toSemilatticeSup` `Nat.instLattice`	—	`Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `sPolynomial_def` `LE.le.trans` `degree_sub_le` `sup_le_sup` `degree_mul_le` `degree_monomial` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Finsupp.instCanonicallyOrderedAddOfAddLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finsupp.isOrderedAddMonoid` `Finsupp.orderedSub` `max_self` `Mathlib.Tactic.Push.not_and_or_eq` `sPolynomial_left_zero` `degree_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `sup_of_le_right` `sPolynomial_right_zero` `sup_of_le_left`
`degree_sPolynomial_lt_sup_degree` 📖	mathematical	—	`syn` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `CommRing.toCommSemiring` `sPolynomial` `SemilatticeSup.toMax` `Finsupp.semilatticeSup` `Lattice.toSemilatticeSup` `Nat.instLattice`	—	`degree_sPolynomial`
`degree_smul` 📖	mathematical	`IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`degree` `MvPolynomial` `Algebra.toSMul` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id`	—	`degree_smul_of_isRegular`
`degree_smul_le` 📖	mathematical	—	`syn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `MvPolynomial` `Algebra.toSMul` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id`	—	`MvPolynomial.smul_eq_C_mul` `degree_mul_le` `degree_C` `zero_add`
`degree_smul_of_isRegular` 📖	mathematical	`IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`degree` `MvPolynomial` `Algebra.toSMul` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id`	—	`degree_smul_of_mem_nonZeroDivisors` `IsRegular.mem_nonZeroDivisors`
`degree_smul_of_mem_nonZeroDivisors` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	`degree` `MvPolynomial` `Algebra.toSMul` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id`	—	`smul_zero` `degree_zero` `AddEquiv.injective` `le_antisymm` `degree_smul_le` `le_degree` `MvPolynomial.smul_eq_C_mul` `zero_add` `degree_C` `coeff_mul_of_degree_add` `leadingCoeff_C` `not_imp_not` `mem_nonZeroDivisors_iff` `leadingCoeff_ne_zero_iff`
`degree_sub_le` 📖	mathematical	—	`syn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`sub_eq_add_neg` `degree_add_le` `degree_neg`
`degree_sub_leadingTerm_le` 📖	mathematical	—	`syn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial` `leadingTerm`	—	`le_trans` `degree_sub_le` `degree_leadingTerm` `max_self`
`degree_sub_leadingTerm_lt_degree` 📖	mathematical	—	`syn` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial` `leadingTerm`	—	`degree_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `EquivLike.toEmbeddingLike` `lt_of_le_of_ne` `degree_sub_leadingTerm_le` `MvPolynomial.coeff_sub` `MvPolynomial.coeff_monomial` `sub_self` `MvPolynomial.mem_support_iff` `degree_mem_support`
`degree_sub_leadingTerm_lt_iff` 📖	mathematical	—	`syn` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial` `leadingTerm`	—	`not_lt_bot` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `degree_sub_leadingTerm_lt_degree`
`degree_sub_of_lt` 📖	mathematical	`syn` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `CommRing.toCommSemiring`	`MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial`	—	`sub_eq_add_neg` `degree_add_of_lt` `degree_neg`
`degree_subsingleton` 📖	mathematical	—	`degree` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instZero`	—	`Subsingleton.eq_zero` `Unique.instSubsingleton` `degree_zero`
`degree_sum_le` 📖	mathematical	—	`syn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `Finset.sum` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `Finset.sup` `Lattice.toSemilatticeSup` `orderBot`	—	`Finset.cons_induction_on` `degree_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `Finset.sup_empty` `Finset.sum_cons` `Finset.sup_cons` `le_trans` `degree_add_le` `max_le_max` `le_rfl`
`degree_zero` 📖	mathematical	—	`degree` `MvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `Finsupp` `Nat.instMulZeroClass` `Finsupp.instZero`	—	`Finset.sup_empty` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`eq_C_of_degree_eq_zero` 📖	mathematical	`degree` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instZero`	`DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.C` `leadingCoeff`	—	`MvPolynomial.ext` `MvPolynomial.coeff_C` `coeff_eq_zero_of_lt` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `lt_iff_le_and_ne` `EmbeddingLike.map_eq_zero_iff` `EquivLike.toEmbeddingLike` `bot_le`
`image_leadingTerm_insert_zero` 📖	mathematical	—	`Set.image` `MvPolynomial` `leadingTerm` `Set` `Set.instInsert` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`Set.ext` `leadingTerm_zero`
`image_leadingTerm_sdiff_singleton_zero` 📖	mathematical	—	`Set.image` `MvPolynomial` `leadingTerm` `Set` `Set.instSDiff` `Set.instSingletonSet` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`Set.ext`
`isUnit_leadingCoeff` 📖	mathematical	—	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `leadingCoeff` `Semifield.toCommSemiring`	—	—
`le_degree` 📖	mathematical	`Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finset` `Finset.instMembership` `MvPolynomial.support`	`syn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree`	—	`AddEquiv.apply_symm_apply` `Finset.le_sup`
`leadingCoeff_C` 📖	mathematical	—	`leadingCoeff` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.C`	—	`degree_C` `MvPolynomial.coeff_zero_C`
`leadingCoeff_X` 📖	mathematical	—	`leadingCoeff` `MvPolynomial.X` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`leadingCoeff_monomial`
`leadingCoeff_add_of_lt` 📖	mathematical	`syn` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree`	`leadingCoeff` `MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`degree_add_of_lt` `MvPolynomial.coeff_add` `coeff_eq_zero_of_lt` `add_zero`
`leadingCoeff_eq_zero_iff` 📖	mathematical	—	`leadingCoeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial` `MvPolynomial.commSemiring`	—	—
`leadingCoeff_leadingTerm` 📖	mathematical	—	`leadingCoeff` `leadingTerm`	—	`leadingCoeff_monomial`
`leadingCoeff_monomial` 📖	mathematical	—	`leadingCoeff` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPolynomial.commSemiring` `Semiring.toModule` `MvPolynomial.module` `LinearMap.instFunLike` `MvPolynomial.monomial`	—	`degree_monomial` `MvPolynomial.monomial_zero` `MvPolynomial.coeff_monomial`
`leadingCoeff_mul` 📖	mathematical	—	`leadingCoeff` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`MulZeroClass.zero_mul` `leadingCoeff_zero` `MulZeroClass.mul_zero` `leadingCoeff.eq_1` `degree_mul` `coeff_mul_of_degree_add`
`leadingCoeff_mul_of_isRegular_left` 📖	mathematical	`IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `leadingCoeff`	`MvPolynomial` `MvPolynomial.commSemiring`	—	`degree_mul_of_isRegular_left` `coeff_mul_of_degree_add`
`leadingCoeff_mul_of_isRegular_right` 📖	mathematical	`IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `leadingCoeff`	`MvPolynomial` `MvPolynomial.commSemiring`	—	`degree_mul_of_isRegular_right` `coeff_mul_of_degree_add`
`leadingCoeff_mul_of_left_mem_nonZeroDivisors` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `leadingCoeff`	`MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPolynomial.commSemiring`	—	`degree_mul_of_left_mem_nonZeroDivisors` `coeff_mul_of_degree_add`
`leadingCoeff_mul_of_mul_leadingCoeff_ne_zero` 📖	mathematical	—	`leadingCoeff` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`leadingCoeff.eq_1` `coeff_mul_of_degree_add` `degree_mul_of_mul_leadingCoeff_ne_zero`
`leadingCoeff_mul_of_right_mem_nonZeroDivisors` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `leadingCoeff`	`MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPolynomial.commSemiring`	—	`degree_mul_of_right_mem_nonZeroDivisors` `coeff_mul_of_degree_add`
`leadingCoeff_ne_zero_iff` 📖	—	—	—	—	`not_imp_not` `leadingCoeff_zero` `leadingCoeff.eq_1` `MvPolynomial.mem_support_iff` `degree.eq_1` `Finset.sup_mem_of_nonempty` `MvPolynomial.support_nonempty` `AddEquiv.symm_apply_apply`
`leadingCoeff_neg` 📖	mathematical	—	`leadingCoeff` `CommRing.toCommSemiring` `MvPolynomial` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial`	—	`degree_neg` `MvPolynomial.coeff_neg`
`leadingCoeff_one` 📖	mathematical	—	`leadingCoeff` `MvPolynomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`leadingCoeff_monomial`
`leadingCoeff_pow` 📖	mathematical	—	`leadingCoeff` `MvPolynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`leadingCoeff.eq_1` `degree_pow` `coeff_pow_nsmul_degree`
`leadingCoeff_pow_of_pow_leadingCoeff_ne_zero` 📖	mathematical	—	`leadingCoeff` `MvPolynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`leadingCoeff.eq_1` `degree_pow_of_pow_leadingCoeff_ne_zero` `coeff_pow_nsmul_degree`
`leadingCoeff_prod_of_mem_nonZeroDivisors` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `leadingCoeff`	`Finset.prod` `MvPolynomial` `CommSemiring.toCommMonoid` `MvPolynomial.commSemiring`	—	`degree_prod_of_mem_nonZeroDivisors` `coeff_prod_sum_degree` `Finset.prod_congr`
`leadingCoeff_prod_of_regular` 📖	mathematical	`IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `leadingCoeff`	`Finset.prod` `MvPolynomial` `CommSemiring.toCommMonoid` `MvPolynomial.commSemiring`	—	`degree_prod_of_regular` `coeff_prod_sum_degree` `Finset.prod_congr`
`leadingCoeff_sub_of_lt` 📖	mathematical	`syn` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `CommRing.toCommSemiring`	`leadingCoeff` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial`	—	`sub_eq_add_neg` `leadingCoeff_add_of_lt` `degree_neg`
`leadingCoeff_zero` 📖	mathematical	—	`leadingCoeff` `MvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`Finset.sup_empty` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`leadingTerm_C` 📖	mathematical	—	`leadingTerm` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.C`	—	`degree_C` `leadingCoeff_C`
`leadingTerm_eq_zero_iff` 📖	mathematical	—	`leadingTerm` `MvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	—
`leadingTerm_leadingTerm` 📖	mathematical	—	`leadingTerm`	—	`degree_zero` `leadingCoeff_zero` `MvPolynomial.monomial_zero` `degree_monomial` `leadingCoeff_monomial`
`leadingTerm_monomial` 📖	mathematical	—	`leadingTerm` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPolynomial.commSemiring` `Semiring.toModule` `MvPolynomial.module` `LinearMap.instFunLike` `MvPolynomial.monomial`	—	`MvPolynomial.monomial_zero` `degree_zero` `leadingCoeff_zero` `degree_monomial` `leadingCoeff_monomial`
`leadingTerm_zero` 📖	mathematical	—	`leadingTerm` `MvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`leadingTerm_eq_zero_iff`
`monic_X` 📖	mathematical	—	`Monic` `MvPolynomial.X`	—	`monic_monomial_one`
`monic_X_add_C` 📖	mathematical	—	`Monic` `CommRing.toCommSemiring` `MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `MvPolynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.C`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Monic.add_of_lt` `monic_X` `degree_C` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `degree_X` `EquivLike.toEmbeddingLike`
`monic_X_sub_C` 📖	mathematical	—	`Monic` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial` `MvPolynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.C`	—	`sub_eq_add_neg` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `monic_X_add_C`
`monic_monomial` 📖	mathematical	—	`Monic` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPolynomial.commSemiring` `Semiring.toModule` `MvPolynomial.module` `LinearMap.instFunLike` `MvPolynomial.monomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Monic.eq_1` `leadingCoeff_monomial`
`monic_monomial_one` 📖	mathematical	—	`Monic` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPolynomial.commSemiring` `Semiring.toModule` `MvPolynomial.module` `LinearMap.instFunLike` `MvPolynomial.monomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`leadingCoeff_monomial`
`monic_one` 📖	mathematical	—	`Monic` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.C` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`monic_monomial_one`
`ne_zero_of_degree_ne_zero` 📖	—	—	—	—	`degree_zero`
`notMem_support_of_degree_lt` 📖	mathematical	`syn` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree`	`Finset` `Finset.instMembership` `MvPolynomial.support`	—	`coeff_eq_zero_of_lt`
`sPolynomial_antisymm` 📖	mathematical	—	`sPolynomial` `MvPolynomial` `CommRing.toCommSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial`	—	`Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `neg_sub`
`sPolynomial_decomposition` 📖	mathematical	`DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `syn` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `CommRing.toCommSemiring` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `leadingCoeff` `MvPolynomial` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	`Algebra.toSMul` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `sPolynomial`	—	`Finset.induction_on` `Finset.sum_congr` `Finset.sum_const_zero` `Zero.instNonempty` `Finset.sum_insert` `zero_add` `sPolynomial_right_zero` `smul_zero` `sPolynomial_left_zero` `ite_smul` `zero_smul` `Finset.sum_ite_eq'` `add_zero` `sPolynomial_self` `add_eq_zero_iff_neg_eq'` `AddEquiv.injective` `degree_zero` `MvPolynomial.coeff_sum` `MvPolynomial.coeff_add` `MvPolynomial.notMem_support_iff` `notMem_support_of_degree_lt` `add_comm` `Finset.sum_sub_distrib` `sub_eq_add_neg` `Finset.sum_smul` `Finset.sum_mul` `neg_smul` `neg_mul` `IsUnit.mul_val_inv` `one_smul` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `sPolynomial.eq_1` `mul_comm` `tsub_self` `Finsupp.instCanonicallyOrderedAddOfAddLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finsupp.orderedSub` `smul_sub` `IsUnit.val_inv_mul` `leadingCoeff_zero` `MulZeroClass.zero_mul` `sub_self` `tsub_zero` `MulZeroClass.mul_zero` `zero_tsub` `MvPolynomial.monomial_zero`
`sPolynomial_decomposition'` 📖	mathematical	`DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `syn` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `degree` `Semifield.toCommSemiring` `Field.toSemifield` `MvPolynomial` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `Field.toCommRing` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	`CommRing.toCommSemiring` `Algebra.toSMul` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `sPolynomial`	—	`sPolynomial_decomposition`
`sPolynomial_def` 📖	mathematical	—	`sPolynomial` `MvPolynomial` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPolynomial.commSemiring` `Semiring.toModule` `MvPolynomial.module` `LinearMap.instFunLike` `MvPolynomial.monomial` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.tsub` `Nat.instAddCommMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `SemilatticeSup.toMax` `Finsupp.semilatticeSup` `Lattice.toSemilatticeSup` `Nat.instLattice` `degree` `leadingCoeff`	—	`Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `Finsupp.ext` `le_total` `sup_of_le_right` `sup_of_le_left` `tsub_self` `sPolynomial.eq_1` `sup_comm`
`sPolynomial_leadingTerm_mul` 📖	mathematical	—	`sPolynomial` `MvPolynomial` `CommRing.toCommSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `leadingTerm` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPolynomial.commSemiring` `Semiring.toModule` `MvPolynomial.module` `LinearMap.instFunLike` `MvPolynomial.monomial` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.tsub` `Nat.instAddCommMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `SemilatticeSup.toMax` `Finsupp.semilatticeSup` `Lattice.toSemilatticeSup` `Nat.instLattice` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `degree` `leadingCoeff`	—	`Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `sPolynomial_monomial_mul`
`sPolynomial_leadingTerm_mul'` 📖	mathematical	—	`sPolynomial` `MvPolynomial` `CommRing.toCommSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `leadingTerm` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPolynomial.commSemiring` `Semiring.toModule` `MvPolynomial.module` `LinearMap.instFunLike` `MvPolynomial.monomial` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.tsub` `Nat.instAddCommMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `SemilatticeSup.toMax` `Finsupp.semilatticeSup` `Lattice.toSemilatticeSup` `Nat.instLattice` `degree` `leadingCoeff`	—	`Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `sPolynomial_monomial_mul` `degree_mul` `Mathlib.Tactic.Push.not_and_or_eq` `leadingTerm_zero` `MulZeroClass.zero_mul` `sPolynomial_left_zero` `degree_zero` `sup_of_le_right` `Finsupp.instCanonicallyOrderedAddOfAddLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `leadingCoeff_zero` `MvPolynomial.monomial_zero` `sPolynomial_right_zero` `sup_of_le_left` `MulZeroClass.mul_zero`
`sPolynomial_left_zero` 📖	mathematical	—	`sPolynomial` `MvPolynomial` `CommRing.toCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial`	—	`Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `degree_zero` `tsub_zero` `Finsupp.orderedSub` `MulZeroClass.mul_zero` `zero_tsub` `Finsupp.instCanonicallyOrderedAddOfAddLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `leadingCoeff_zero` `MvPolynomial.monomial_zero` `MulZeroClass.zero_mul` `sub_self`
`sPolynomial_lt_of_degree_ne_zero_of_degree_eq` 📖	mathematical	`degree` `CommRing.toCommSemiring`	`syn` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toSyn` `sPolynomial`	—	`sup_of_le_left` `degree_sPolynomial_lt_sup_degree`
`sPolynomial_monomial_mul` 📖	mathematical	—	`sPolynomial` `MvPolynomial` `CommRing.toCommSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPolynomial.commSemiring` `Semiring.toModule` `MvPolynomial.module` `LinearMap.instFunLike` `MvPolynomial.monomial` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.tsub` `Nat.instAddCommMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `SemilatticeSup.toMax` `Finsupp.semilatticeSup` `Lattice.toSemilatticeSup` `Nat.instLattice` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `degree`	—	`Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `sPolynomial_def` `Iff.not` `MvPolynomial.monomial_eq_zero` `degree_mul` `mul_sub` `mul_assoc` `MvPolynomial.monomial_mul` `leadingCoeff_mul` `leadingCoeff_monomial` `degree_monomial` `mul_right_comm` `mul_comm` `tsub_add_tsub_cancel` `CanonicallyOrderedAdd.toExistsAddOfLE` `Finsupp.instCanonicallyOrderedAddOfAddLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finsupp.isOrderedAddMonoid` `Finsupp.orderedSub` `sup_le_sup` `self_le_add_left` `tsub_add_eq_add_tsub` `Finsupp.addLeftReflectLE` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `le_sup_left` `le_sup_right` `add_comm` `add_tsub_add_eq_tsub_right` `Mathlib.Tactic.Push.not_and_or_eq` `MvPolynomial.monomial_zero` `MulZeroClass.zero_mul` `degree_zero` `sup_of_le_right` `tsub_zero` `MulZeroClass.mul_zero` `tsub_self` `leadingCoeff_zero` `sub_self` `sup_of_le_left` `add_zero`
`sPolynomial_monomial_mul'` 📖	mathematical	—	`sPolynomial` `MvPolynomial` `CommRing.toCommSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPolynomial.commSemiring` `Semiring.toModule` `MvPolynomial.module` `LinearMap.instFunLike` `MvPolynomial.monomial` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.tsub` `Nat.instAddCommMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `SemilatticeSup.toMax` `Finsupp.semilatticeSup` `Lattice.toSemilatticeSup` `Nat.instLattice` `degree`	—	`Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `sPolynomial_monomial_mul` `degree_mul` `degree_monomial` `Mathlib.Tactic.Push.not_and_or_eq` `MvPolynomial.monomial_zero` `MulZeroClass.zero_mul` `sPolynomial_left_zero` `degree_zero` `sup_of_le_right` `Finsupp.instCanonicallyOrderedAddOfAddLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `sPolynomial_right_zero` `sup_of_le_left` `MulZeroClass.mul_zero`
`sPolynomial_mul_monomial` 📖	mathematical	—	`sPolynomial` `MvPolynomial` `CommRing.toCommSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPolynomial.commSemiring` `Semiring.toModule` `MvPolynomial.module` `LinearMap.instFunLike` `MvPolynomial.monomial` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.tsub` `Nat.instAddCommMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `SemilatticeSup.toMax` `Finsupp.semilatticeSup` `Lattice.toSemilatticeSup` `Nat.instLattice` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `degree`	—	`sPolynomial_monomial_mul`
`sPolynomial_right_zero` 📖	mathematical	—	`sPolynomial` `MvPolynomial` `CommRing.toCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial`	—	`sPolynomial_antisymm` `sPolynomial_left_zero` `neg_zero`
`sPolynomial_self` 📖	mathematical	—	`sPolynomial` `MvPolynomial` `CommRing.toCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial`	—	`sub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub`

MonomialOrder.Monic

Definitions

Name	Category	Theorems
`decidable` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_of_lt` 📖	mathematical	`MonomialOrder.Monic` `MonomialOrder.syn` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MonomialOrder.lo` `DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `MonomialOrder.acm` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `MonomialOrder.toSyn` `MonomialOrder.degree`	`MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`MonomialOrder.leadingCoeff_add_of_lt` `leadingCoeff_eq_one`
`coeff_degree` 📖	mathematical	`MonomialOrder.Monic`	`MvPolynomial.coeff` `MonomialOrder.degree` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	—
`leadingCoeff_eq_one` 📖	mathematical	`MonomialOrder.Monic`	`MonomialOrder.leadingCoeff` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	—
`mul` 📖	mathematical	`MonomialOrder.Monic`	`MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `leadingCoeff_eq_one` `one_mul` `eq_1` `MonomialOrder.leadingCoeff.eq_1` `MonomialOrder.degree_mul_of_mul_leadingCoeff_ne_zero` `one_ne_zero` `NeZero.one` `MonomialOrder.coeff_mul_of_degree_add`
`ne_zero` 📖	—	`MonomialOrder.Monic`	—	—	`MonomialOrder.leadingCoeff_zero` `NeZero.one`
`of_subsingleton` 📖	mathematical	—	`MonomialOrder.Monic`	—	`Subsingleton.eq_one`
`pow` 📖	mathematical	`MonomialOrder.Monic`	`MvPolynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MvPolynomial.commSemiring`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `eq_1` `MonomialOrder.leadingCoeff_pow_of_pow_leadingCoeff_ne_zero` `leadingCoeff_eq_one` `one_pow` `one_ne_zero` `NeZero.one`
`prod` 📖	mathematical	`MonomialOrder.Monic`	`Finset.prod` `MvPolynomial` `CommSemiring.toCommMonoid` `MvPolynomial.commSemiring`	—	`eq_1` `MonomialOrder.leadingCoeff_prod_of_regular` `leadingCoeff_eq_one` `isRegular_one` `Finset.prod_eq_one`

(root)

Definitions

Name	Category	Theorems
`MonomialOrder` 📖	CompData	—

---

← Back to Index