Degrees

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

Statistics

Metric	Count
Definitions `degreeOf`, `degrees`, `degreesLE`, `totalDegree`	4
Theorems `coeff_eq_zero_of_totalDegree_lt`, `degreeOf_C`, `degreeOf_C_mul_le`, `degreeOf_X`, `degreeOf_add_le`, `degreeOf_def`, `degreeOf_eq_sup`, `degreeOf_le_iff`, `degreeOf_le_totalDegree`, `degreeOf_lt_iff`, `degreeOf_monomial_eq`, `degreeOf_mul_C_le`, `degreeOf_mul_X_eq_degreeOf_add_one_iff`, `degreeOf_mul_X_of_ne`, `degreeOf_mul_X_self`, `degreeOf_mul_le`, `degreeOf_one`, `degreeOf_pow_le`, `degreeOf_prod_le`, `degreeOf_rename_of_injective`, `degreeOf_sum_le`, `degreeOf_zero`, `degreesLE_add`, `degreesLE_nsmul`, `degreesLE_zero`, `degrees_C`, `degrees_X`, `degrees_X'`, `degrees_add_le`, `degrees_add_of_disjoint`, `degrees_def`, `degrees_map_le`, `degrees_map_of_injective`, `degrees_monomial`, `degrees_monomial_eq`, `degrees_mul_le`, `degrees_one`, `degrees_pow_le`, `degrees_prod_le`, `degrees_rename`, `degrees_rename_of_injective`, `degrees_sum_le`, `degrees_zero`, `exists_degree_lt`, `le_degrees_add_left`, `le_degrees_add_right`, `le_totalDegree`, `mem_degrees`, `mem_degreesLE`, `monomial_le_degreeOf`, `totalDegree_C`, `totalDegree_X`, `totalDegree_X_pow`, `totalDegree_add`, `totalDegree_add_eq_left_of_totalDegree_lt`, `totalDegree_add_eq_right_of_totalDegree_lt`, `totalDegree_eq`, `totalDegree_eq_zero_iff_eq_C`, `totalDegree_finsetSum_le`, `totalDegree_finset_prod`, `totalDegree_finset_sum`, `totalDegree_le_degrees_card`, `totalDegree_le_of_support_subset`, `totalDegree_list_prod`, `totalDegree_monomial`, `totalDegree_monomial_le`, `totalDegree_mul`, `totalDegree_multiset_prod`, `totalDegree_one`, `totalDegree_pow`, `totalDegree_renameEquiv`, `totalDegree_rename_le`, `totalDegree_smul_le`, `totalDegree_zero`	74
Total	78

MvPolynomial

Definitions

Name	Category	Theorems
`degreeOf` 📖	CompOp	37 math math: `natDegree_finSuccEquiv`, `degreeOf_C`, `chevalley_mvPolynomial_mvPolynomial`, `degreeOf_mul_le`, `degreeOf_sum_le`, `degreeOf_coeff_finSuccEquiv`, `degreeOf_def`, `degreeOf_le_totalDegree`, `degree_optionEquivLeft`, `degreeOf_rename_of_injective`, `degreeOf_mul_eq`, `degreeOf_le_iff`, `degreeOf_pow_eq`, `degreeOf_sub_le`, `degreeOf_mul_X_eq_degreeOf_add_one_iff`, `monomial_le_degreeOf`, `degreeOf_mul_X_self`, `natDegree_optionEquivLeft`, `degreeOf_eq_sup`, `degreeOf_prod_eq`, `degree_finSuccEquiv`, `degreeOf_pow_le`, `degreeOf_X`, `degreeOf_one`, `degreeOf_mul_C_le`, `degreeOf_C_mul_le`, `degreeOf_C_mul`, `degreeOf_zero`, `degreeOf_sub_lt`, `schwartz_zippel_sum_degreeOf`, `degreeOf_prod_le`, `degreeOf_eq_natDegree`, `degreeOf_neg`, `degreeOf_mul_X_of_ne`, `degreeOf_monomial_eq`, `degreeOf_add_le`, `degreeOf_lt_iff`
`degrees` 📖	CompOp	28 math math: `degrees_neg`, `degrees_monomial`, `degreeOf_def`, `degrees_def`, `degrees_map_of_injective`, `degrees_C`, `degrees_X`, `degrees_pow_le`, `degrees_rename`, `degrees_map_le`, `degrees_indicator`, `degrees_sub_le`, `degrees_sum_le`, `totalDegree_le_degrees_card`, `degrees_one`, `mem_degreesLE`, `vars_def`, `degrees_prod_le`, `degrees_add_le`, `degrees_mul_le`, `mem_restrictDegree_iff_sup`, `degrees_mul_eq`, `degrees_esymm`, `degrees_zero`, `degrees_rename_of_injective`, `degrees_monomial_eq`, `degrees_X'`, `mem_degrees`
`degreesLE` 📖	CompOp	4 math math: `degreesLE_nsmul`, `degreesLE_add`, `degreesLE_zero`, `mem_degreesLE`
`totalDegree` 📖	CompOp	47 math math: `totalDegree_monomial`, `LinearMap.toMvPolynomial_totalDegree_le`, `totalDegree_X_pow`, `totalDegree_coeff_finSuccEquiv_add_le`, `totalDegree_le_of_support_subset`, `schwartz_zippel_totalDegree`, `totalDegree_eq`, `degreeOf_le_totalDegree`, `Matrix.toMvPolynomial_totalDegree_le`, `totalDegree_list_prod`, `sum_homogeneousComponent`, `totalDegree_rename_le`, `totalDegree_mul_of_isDomain`, `isUnit_iff_totalDegree_of_isReduced`, `totalDegree_finset_prod`, `totalDegree_C`, `totalDegree_pow`, `IsHomogeneous.totalDegree_le`, `totalDegree_multiset_prod`, `degree_degLexDegree`, `totalDegree_eq_zero_iff_eq_C`, `combinatorial_nullstellensatz_exists_linearCombination`, `weightedTotalDegree_one`, `totalDegree_neg`, `totalDegree_le_of_dvd_of_isDomain`, `totalDegree_expand`, `totalDegree_le_degrees_card`, `totalDegree_add`, `totalDegree_renameEquiv`, `totalDegree_eq_zero_iff`, `MonomialOrder.degree_eq_zero_iff_totalDegree_eq_zero`, `MvPowerSeries.totalDegree_trunc'`, `totalDegree_sub`, `totalDegree_X`, `totalDegree_zero`, `totalDegree_one`, `totalDegree_monomial_le`, `totalDegree_mul`, `IsHomogeneous.totalDegree`, `totalDegree_finset_sum`, `le_totalDegree`, `totalDegree_sub_C_le`, `totalDegree_smul_le`, `totalDegree_zero_iff_isHomogeneous`, `totalDegree_coeff_optionEquivLeft_le`, `degLex_totalDegree_monotone`, `mem_restrictTotalDegree`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_eq_zero_of_totalDegree_lt` 📖	mathematical	`totalDegree` `Finset.sum` `Nat.instAddCommMonoid` `Finsupp.support` `MulZeroClass.toZero` `Nat.instMulZeroClass` `DFunLike.coe` `Finsupp` `Finsupp.instFunLike`	`coeff` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`mem_support_iff` `Finset.sup_lt_iff` `lt_of_le_of_lt` `totalDegree.eq_1` `lt_irrefl`
`degreeOf_C` 📖	mathematical	—	`degreeOf` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `C`	—	`degreeOf_def` `Multiset.count.congr_simp` `degrees_C` `Multiset.count_eq_zero_of_notMem`
`degreeOf_C_mul_le` 📖	mathematical	—	`degreeOf` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `C`	—	`degrees_C` `zero_add` `Multiset.count_le_of_le` `degrees_mul_le`
`degreeOf_X` 📖	mathematical	—	`degreeOf` `X`	—	`degreeOf_def` `Multiset.count.congr_simp` `degrees_X` `Multiset.count_singleton` `Multiset.count_eq_zero_of_notMem`
`degreeOf_add_le` 📖	mathematical	—	`degreeOf` `MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`degreeOf_eq_sup` `AddMonoidAlgebra.supDegree_add_le`
`degreeOf_def` 📖	mathematical	—	`degreeOf` `Multiset.count` `degrees`	—	`degreeOf.eq_1` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable`
`degreeOf_eq_sup` 📖	mathematical	—	`degreeOf` `Finset.sup` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Lattice.toSemilatticeSup` `Nat.instLattice` `Nat.instOrderBot` `support` `DFunLike.coe` `Finsupp.instFunLike`	—	`degreeOf_def` `degrees.eq_1` `Multiset.count_finset_sup` `Finsupp.count_toMultiset`
`degreeOf_le_iff` 📖	mathematical	—	`degreeOf` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike`	—	`degreeOf_eq_sup` `Finset.sup_le_iff`
`degreeOf_le_totalDegree` 📖	mathematical	—	`degreeOf` `totalDegree`	—	`degreeOf_le_iff` `eq_or_ne` `LE.le.trans` `Finset.single_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finsupp.mem_support_iff` `le_totalDegree`
`degreeOf_lt_iff` 📖	mathematical	—	`degreeOf` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike`	—	`degreeOf_eq_sup` `Finset.sup_lt_iff`
`degreeOf_monomial_eq` 📖	mathematical	—	`degreeOf` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike`	—	`degreeOf_def` `degrees_monomial_eq` `Finsupp.count_toMultiset`
`degreeOf_mul_C_le` 📖	mathematical	—	`degreeOf` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `C`	—	`degrees_C` `add_zero` `Multiset.count_le_of_le` `degrees_mul_le`
`degreeOf_mul_X_eq_degreeOf_add_one_iff` 📖	mathematical	—	`degreeOf` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `X`	—	`MulZeroClass.zero_mul` `degreeOf_zero` `zero_add` `degreeOf_mul_X_self` `Finset.comp_sup_eq_sup_comp_of_nonempty` `support_nonempty` `Finsupp.instIsRightCancelAdd` `AddRightCancelSemigroup.toIsRightCancelAdd` `degreeOf_eq_sup` `support_mul_X` `Finset.sup_le` `Finset.sup_map` `bot_eq_zero'` `Nat.instCanonicallyOrderedAdd` `Nat.instZeroLEOneClass` `Finsupp.single_eq_same` `mem_support_iff`
`degreeOf_mul_X_of_ne` 📖	mathematical	—	`degreeOf` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `X`	—	`Finsupp.instIsRightCancelAdd` `AddRightCancelSemigroup.toIsRightCancelAdd` `degreeOf_eq_sup` `support_mul_X` `Finset.sup_map` `Pi.single_eq_of_ne` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`degreeOf_mul_X_self` 📖	mathematical	—	`degreeOf` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `X`	—	`LE.le.trans` `Multiset.count_le_of_le` `degrees_mul_le` `Multiset.count_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Multiset.count_singleton_self` `degrees_X'`
`degreeOf_mul_le` 📖	mathematical	—	`degreeOf` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`Multiset.count_add` `Multiset.count_le_of_le` `degrees_mul_le`
`degreeOf_one` 📖	mathematical	—	`degreeOf` `MvPolynomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`degreeOf_def` `Multiset.count.congr_simp` `degrees_one` `Multiset.count_eq_zero_of_notMem`
`degreeOf_pow_le` 📖	mathematical	—	`degreeOf` `MvPolynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `commSemiring`	—	`Finset.prod_const` `Finset.card_range` `Finset.sum_const` `degreeOf_prod_le`
`degreeOf_prod_le` 📖	mathematical	—	`degreeOf` `Finset.prod` `MvPolynomial` `CommSemiring.toCommMonoid` `commSemiring` `Finset.sum` `Nat.instAddCommMonoid`	—	`degreeOf_eq_sup` `Finset.sum_congr` `AddMonoidAlgebra.supDegree_prod_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`degreeOf_rename_of_injective` 📖	mathematical	—	`degreeOf` `DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `rename`	—	`Multiset.count.congr_simp` `degrees_rename_of_injective` `Multiset.count_map_eq_count'`
`degreeOf_sum_le` 📖	mathematical	—	`degreeOf` `Finset.sum` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Finset.sup` `Lattice.toSemilatticeSup` `Nat.instLattice` `Nat.instOrderBot`	—	`degreeOf_eq_sup` `AddMonoidAlgebra.supDegree_sum_le`
`degreeOf_zero` 📖	mathematical	—	`degreeOf` `MvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`degreeOf_def` `Multiset.count.congr_simp` `degrees_zero`
`degreesLE_add` 📖	mathematical	—	`degreesLE` `Multiset` `Multiset.instAdd` `Submodule` `MvPolynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `Submodule.mul` `IsScalarTower.right` `algebra` `Algebra.id`	—	`IsScalarTower.right` `le_antisymm_iff` `Submodule.mul_le` `sum_mem` `Submodule.addSubmonoidClass` `LE.le.trans` `Finset.le_sup` `AddEquiv.injective` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `Multiset.toFinsupp_toMultiset` `Multiset.sub_add_inter` `Multiset.instOrderedSub` `monomial_mul` `mul_one` `Submodule.mul_mem_mul` `degrees_monomial` `as_sum` `degrees_mul_le` `add_le_add` `Multiset.instAddLeftMono` `covariant_swap_add_of_covariant_add`
`degreesLE_nsmul` 📖	mathematical	—	`degreesLE` `Multiset` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `Submodule` `MvPolynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `algebra` `Algebra.id`	—	`zero_nsmul` `degreesLE_zero` `pow_zero` `IsScalarTower.right` `add_smul` `one_smul` `degreesLE_add` `pow_succ`
`degreesLE_zero` 📖	mathematical	—	`degreesLE` `Multiset` `Multiset.instZero` `Submodule` `MvPolynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `Submodule.one`	—	`le_antisymm` `totalDegree_eq_zero_iff_eq_C` `LE.le.trans` `totalDegree_le_degrees_card` `Multiset.instCanonicallyOrderedAdd` `Algebra.smul_def` `mul_one` `degrees_one`
`degrees_C` 📖	mathematical	—	`degrees` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `C` `Multiset` `Multiset.instZero`	—	`Multiset.le_zero` `degrees_monomial`
`degrees_X` 📖	mathematical	—	`degrees` `X` `Multiset` `Multiset.instSingleton`	—	`degrees_monomial_eq` `one_ne_zero` `NeZero.one` `Finsupp.toMultiset_single`
`degrees_X'` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `degrees` `X` `Multiset.instSingleton`	—	`le_trans` `degrees_monomial` `le_of_eq` `Finsupp.toMultiset_single`
`degrees_add_le` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `degrees` `MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `Multiset.instLattice`	—	`degrees_def` `AddMonoidAlgebra.supDegree_add_le`
`degrees_add_of_disjoint` 📖	mathematical	`Disjoint` `Multiset` `Multiset.instPartialOrder` `Multiset.instOrderBot` `degrees`	`MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Multiset.instUnion`	—	`LE.le.antisymm` `degrees_add_le` `Multiset.union_le` `le_degrees_add_left` `le_degrees_add_right`
`degrees_def` 📖	mathematical	—	`degrees` `Finset.sup` `Multiset` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Lattice.toSemilatticeSup` `Multiset.instLattice` `Multiset.instOrderBot` `support` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `Finsupp.toMultiset`	—	`degrees.eq_1` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable`
`degrees_map_le` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `degrees` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `map`	—	`Finset.sup_mono` `support_map_subset`
`degrees_map_of_injective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike`	`degrees` `MvPolynomial` `commSemiring` `map`	—	`support_map_of_injective`
`degrees_monomial` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `degrees` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `Finsupp.toMultiset`	—	`Eq.trans_le` `AddMonoidAlgebra.supDegree_single` `bot_le` `le_rfl`
`degrees_monomial_eq` 📖	mathematical	—	`degrees` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `Finsupp.toMultiset`	—	`AddMonoidAlgebra.supDegree_single`
`degrees_mul_le` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `degrees` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Multiset.instAdd`	—	`degrees_def` `AddMonoidAlgebra.supDegree_mul_le` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `Multiset.instAddLeftMono` `covariant_swap_add_of_covariant_add`
`degrees_one` 📖	mathematical	—	`degrees` `MvPolynomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Multiset` `Multiset.instZero`	—	`degrees_C`
`degrees_pow_le` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `degrees` `MvPolynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `commSemiring` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid`	—	`Finset.prod_const` `Finset.card_range` `Finset.sum_const` `degrees_prod_le`
`degrees_prod_le` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `degrees` `Finset.prod` `MvPolynomial` `CommSemiring.toCommMonoid` `commSemiring` `Finset.sum` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid`	—	`AddMonoidAlgebra.supDegree_prod_le` `Multiset.instAddLeftMono` `covariant_swap_add_of_covariant_add` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `map_add` `AddMonoidHomClass.toAddHomClass`
`degrees_rename` 📖	mathematical	—	`Multiset` `Multiset.instHasSubset` `degrees` `DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `rename` `Multiset.map`	—	`mem_degrees` `Multiset.mem_map` `coeff_rename_ne_zero` `Mathlib.Tactic.Contrapose.contrapose₂` `Mathlib.Tactic.Push.not_and_eq` `Finset.sum_eq_zero` `Finsupp.single_apply` `Finsupp.sum.eq_1` `Finsupp.sum_apply`
`degrees_rename_of_injective` 📖	mathematical	—	`degrees` `DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `rename` `Multiset.map`	—	`support_rename_of_injective` `Finset.sup_image` `Multiset.map_finset_sup` `Finset.sup_congr` `Finsupp.toMultiset_map`
`degrees_sum_le` 📖	mathematical	—	`Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `degrees` `Finset.sum` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Finset.sup` `Lattice.toSemilatticeSup` `Multiset.instLattice` `Multiset.instOrderBot`	—	`degrees_def` `AddMonoidAlgebra.supDegree_sum_le`
`degrees_zero` 📖	mathematical	—	`degrees` `MvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Multiset` `Multiset.instZero`	—	`C_0` `degrees_C`
`exists_degree_lt` 📖	mathematical	`totalDegree` `Fintype.card` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finset` `Finset.instMembership` `support`	`DFunLike.coe` `Finsupp.instFunLike`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Finset.sum_const` `Nat.nsmul_eq_mul` `mul_comm` `Finset.card_univ` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finsupp.sum_fintype` `le_refl` `le_totalDegree`
`le_degrees_add_left` 📖	mathematical	`Disjoint` `Multiset` `Multiset.instPartialOrder` `Multiset.instOrderBot` `degrees`	`Preorder.toLE` `PartialOrder.toPreorder` `MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`Finset.sup_le` `eq_or_ne` `Finsupp.toMultiset_zero` `Multiset.zero_le` `Finset.le_sup_of_le` `mem_support_iff` `coeff_add` `Finset.nonempty_iff_ne_empty` `Finsupp.support_eq_empty` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `mem_degrees` `Multiset.disjoint_iff_ne` `add_zero` `coeff.eq_1` `Finsupp.mem_support_iff` `le_rfl`
`le_degrees_add_right` 📖	mathematical	`Disjoint` `Multiset` `Multiset.instPartialOrder` `Multiset.instOrderBot` `degrees`	`Preorder.toLE` `PartialOrder.toPreorder` `MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`add_comm` `le_degrees_add_left` `Disjoint.symm`
`le_totalDegree` 📖	mathematical	`Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finset` `Finset.instMembership` `support`	`Finsupp.sum` `Nat.instAddCommMonoid` `totalDegree`	—	`Finset.le_sup`
`mem_degrees` 📖	mathematical	—	`Multiset` `Multiset.instMembership` `degrees` `Finset` `Finset.instMembership` `Finsupp.support` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`degrees_def`
`mem_degreesLE` 📖	mathematical	—	`MvPolynomial` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `degreesLE` `Multiset` `Preorder.toLE` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `degrees`	—	—
`monomial_le_degreeOf` 📖	mathematical	`Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finset` `Finset.instMembership` `support`	`DFunLike.coe` `Finsupp.instFunLike` `degreeOf`	—	`degreeOf_eq_sup` `Finset.le_sup`
`totalDegree_C` 📖	mathematical	—	`totalDegree` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `C`	—	`AddMonoidAlgebra.supDegree_single` `Finsupp.sum_zero_index` `bot_eq_zero'` `Nat.instCanonicallyOrderedAdd`
`totalDegree_X` 📖	mathematical	—	`totalDegree` `X`	—	`totalDegree.eq_1` `support_X` `Finsupp.sum_single_index` `sup_bot_eq`
`totalDegree_X_pow` 📖	mathematical	—	`totalDegree` `MvPolynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `commSemiring` `X`	—	`X_pow_eq_monomial` `totalDegree_monomial` `NeZero.one` `Finsupp.sum_single_index`
`totalDegree_add` 📖	mathematical	—	`totalDegree` `MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`AddMonoidAlgebra.sup_support_add_le`
`totalDegree_add_eq_left_of_totalDegree_lt` 📖	mathematical	`totalDegree`	`MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`le_antisymm` `max_eq_left_of_lt` `totalDegree_add` `totalDegree_zero` `zero_add` `Nat.instCanonicallyOrderedAdd` `Finset.exists_mem_eq_sup` `Finsupp.support_nonempty_iff` `Mathlib.Tactic.Contrapose.contrapose₃` `totalDegree_eq` `Finset.le_sup` `support_sdiff_support_subset_support_add` `Finset.mem_sdiff`
`totalDegree_add_eq_right_of_totalDegree_lt` 📖	mathematical	`totalDegree`	`MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`add_comm` `totalDegree_add_eq_left_of_totalDegree_lt`
`totalDegree_eq` 📖	mathematical	—	`totalDegree` `Finset.sup` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Lattice.toSemilatticeSup` `Nat.instLattice` `Nat.instOrderBot` `support` `Multiset.card` `DFunLike.coe` `AddMonoidHom` `Multiset` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `Finsupp.toMultiset`	—	`totalDegree.eq_1` `Finsupp.card_toMultiset`
`totalDegree_eq_zero_iff_eq_C` 📖	mathematical	—	`totalDegree` `DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `RingHom.instFunLike` `C` `coeff` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instZero`	—	`ext` `coeff_C` `coeff_eq_zero_of_totalDegree_lt` `Finset.sum_pos` `Nat.instIsOrderedCancelAddMonoid` `Finsupp.mem_support_iff` `Finsupp.support_nonempty_iff` `totalDegree_C`
`totalDegree_finsetSum_le` 📖	mathematical	`totalDegree`	`Finset.sum` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`LE.le.trans` `totalDegree_finset_sum` `Finset.sup_le`
`totalDegree_finset_prod` 📖	mathematical	—	`totalDegree` `Finset.prod` `MvPolynomial` `CommSemiring.toCommMonoid` `commSemiring` `Finset.sum` `Nat.instAddCommMonoid`	—	`Finset.apply_prod_le_sum_apply` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Eq.le` `totalDegree_one` `totalDegree_mul`
`totalDegree_finset_sum` 📖	mathematical	—	`totalDegree` `Finset.sum` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Finset.sup` `Lattice.toSemilatticeSup` `Nat.instLattice` `Nat.instOrderBot`	—	`Finset.cons_induction` `zero_le` `Nat.instCanonicallyOrderedAdd` `Finset.sum_cons` `Finset.sup_cons` `LE.le.trans` `totalDegree_add` `max_le_max` `le_rfl`
`totalDegree_le_degrees_card` 📖	mathematical	—	`totalDegree` `Multiset.card` `degrees`	—	`totalDegree_eq` `Finset.sup_le` `Multiset.card_le_card` `Finset.le_sup`
`totalDegree_le_of_support_subset` 📖	mathematical	`Finset` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finset.instHasSubset` `support`	`totalDegree`	—	`Finset.sup_mono`
`totalDegree_list_prod` 📖	mathematical	—	`totalDegree` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`List.apply_prod_le_sum_map` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Eq.le` `totalDegree_one` `totalDegree_mul`
`totalDegree_monomial` 📖	mathematical	—	`totalDegree` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `Finsupp.sum` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Nat.instAddCommMonoid`	—	`support_monomial` `Finset.sup_singleton`
`totalDegree_monomial_le` 📖	mathematical	—	`totalDegree` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPolynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `Finsupp.sum` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Nat.instAddCommMonoid`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `totalDegree_zero` `Nat.instCanonicallyOrderedAdd` `totalDegree_monomial` `le_refl`
`totalDegree_mul` 📖	mathematical	—	`totalDegree` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`AddMonoidAlgebra.sup_support_mul_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Eq.le` `Finsupp.sum_add_index'`
`totalDegree_multiset_prod` 📖	mathematical	—	`totalDegree` `Multiset.prod` `MvPolynomial` `CommSemiring.toCommMonoid` `commSemiring` `Multiset.sum` `Nat.instAddCommMonoid` `Multiset.map`	—	`Multiset.apply_prod_le_sum_map` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Eq.le` `totalDegree_one` `totalDegree_mul`
`totalDegree_one` 📖	mathematical	—	`totalDegree` `MvPolynomial` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`totalDegree_C`
`totalDegree_pow` 📖	mathematical	—	`totalDegree` `MvPolynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `commSemiring`	—	`Finset.pow_eq_prod_const` `Nat.nsmul_eq_mul` `Finset.nsmul_eq_sum_const` `AddMonoidAlgebra.supDegree_prod_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Finsupp.sum_add_index'`
`totalDegree_renameEquiv` 📖	mathematical	—	`totalDegree` `DFunLike.coe` `AlgEquiv` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgEquiv.instFunLike` `renameEquiv`	—	`LE.le.antisymm` `totalDegree_rename_le` `le_trans` `rename_rename` `Equiv.symm_comp_self` `rename_id`
`totalDegree_rename_le` 📖	mathematical	—	`totalDegree` `DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `rename`	—	`Finset.sup_le` `Finsupp.mapDomain_support` `rename_eq` `Finset.mem_image` `Eq.trans_le` `Finsupp.sum_mapDomain_index` `le_totalDegree`
`totalDegree_smul_le` 📖	mathematical	—	`totalDegree` `MvPolynomial` `SMulZeroClass.toSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Finset.sup_mono` `support_smul`
`totalDegree_zero` 📖	mathematical	—	`totalDegree` `MvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`C_0` `totalDegree_C`

---

← Back to Index