Degree

📁 Source: Mathlib/Algebra/MonoidAlgebra/Degree.lean

Statistics

Metric	Count
Definitions `infDegree`, `leadingCoeff`, `supDegree`	3
Theorems `leadingCoeff_mul_eq_left`, `leadingCoeff_mul_eq_right`, `mul`, `ne_zero`, `pow`, `supDegree_mul`, `supDegree_mul_of_ne_zero_left`, `supDegree_mul_of_ne_zero_right`, `supDegree_pow`, `apply_add_of_supDegree_le`, `apply_eq_zero_of_not_le_supDegree`, `apply_supDegree_add_supDegree`, `exists_supDegree_mem_support`, `infDegree_withTop_some_comp`, `le_infDegree_add`, `le_infDegree_mul`, `le_inf_support_add`, `le_inf_support_finset_prod`, `le_inf_support_list_prod`, `le_inf_support_mul`, `le_inf_support_multiset_prod`, `le_inf_support_pow`, `leadingCoeff_add_eq_left`, `leadingCoeff_add_eq_right`, `leadingCoeff_eq_zero`, `leadingCoeff_mul`, `leadingCoeff_ne_zero`, `leadingCoeff_single`, `leadingCoeff_zero`, `monic_one`, `ne_zero_of_not_supDegree_le`, `ne_zero_of_supDegree_ne_bot`, `sum_ne_zero_of_injOn_supDegree`, `sum_ne_zero_of_injOn_supDegree'`, `supDegree_add_eq_left`, `supDegree_add_eq_right`, `supDegree_add_le`, `supDegree_eq_of_isMaxOn`, `supDegree_eq_of_max`, `supDegree_leadingCoeff_sum_eq`, `supDegree_mem_range`, `supDegree_mem_support`, `supDegree_mul`, `supDegree_mul_le`, `supDegree_neg`, `supDegree_prod_le`, `supDegree_single`, `supDegree_single_ne_zero`, `supDegree_sub_le`, `supDegree_sub_lt_of_leadingCoeff_eq`, `supDegree_sum_le`, `supDegree_sum_lt`, `supDegree_withBot_some_comp`, `supDegree_zero`, `sup_support_add_le`, `sup_support_finset_prod_le`, `sup_support_list_prod_le`, `sup_support_mul_le`, `sup_support_multiset_prod_le`, `sup_support_pow_le`	60
Total	63

AddMonoidAlgebra

Definitions

Name	Category	Theorems
`infDegree` 📖	CompOp	3 math math: `le_infDegree_add`, `le_infDegree_mul`, `infDegree_withTop_some_comp`
`leadingCoeff` 📖	CompOp	13 math math: `Monic.leadingCoeff_mul_eq_left`, `MvPolynomial.leadingCoeff_esymmAlgHomMonomial`, `leadingCoeff_add_eq_right`, `leadingCoeff_eq_zero`, `leadingCoeff_add_eq_left`, `Monic.leadingCoeff_mul_eq_right`, `leadingCoeff_zero`, `MvPolynomial.leadingCoeff_toLex_C`, `leadingCoeff_single`, `supDegree_leadingCoeff_sum_eq`, `leadingCoeff_mul`, `MvPolynomial.leadingCoeff_toLex`, `apply_supDegree_add_supDegree`
`supDegree` 📖	CompOp	28 math math: `supDegree_single`, `Monic.supDegree_mul`, `Monic.supDegree_mul_of_ne_zero_right`, `supDegree_add_le`, `MvPolynomial.supDegree_esymmAlgHomMonomial`, `supDegree_mem_range`, `supDegree_mul`, `supDegree_eq_of_max`, `supDegree_zero`, `supDegree_neg`, `MvPolynomial.supDegree_esymm`, `exists_supDegree_mem_support`, `MvPolynomial.supDegree_toLex_C`, `Polynomial.supDegree_eq_degree`, `Monic.supDegree_mul_of_ne_zero_left`, `Monic.supDegree_pow`, `supDegree_mul_le`, `supDegree_sub_le`, `supDegree_single_ne_zero`, `supDegree_eq_of_isMaxOn`, `MvPolynomial.IsSymmetric.antitone_supDegree`, `MvPolynomial.leadingCoeff_toLex`, `supDegree_withBot_some_comp`, `Polynomial.supDegree_eq_natDegree`, `supDegree_prod_le`, `supDegree_mem_support`, `apply_supDegree_add_supDegree`, `supDegree_sum_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_add_of_supDegree_le` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `supDegree`	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddMonoidAlgebra` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_apply` `Finset.sum_congr` `Finset.sum_eq_single` `Finset.sum_eq_zero` `addLeftMono_of_addLeftStrictMono` `LT.lt.ne` `add_lt_add_of_lt_of_le` `LE.le.lt_of_ne` `LE.le.trans` `Finset.le_sup` `Finsupp.notMem_support_iff` `MulZeroClass.zero_mul` `add_lt_add_right` `MulZeroClass.mul_zero`
`apply_eq_zero_of_not_le_supDegree` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `supDegree`	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `Finset.le_sup` `Finsupp.mem_support_iff`
`apply_supDegree_add_supDegree` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero`	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `AddMonoidAlgebra` `instMul` `Function.invFun` `Zero.instNonempty` `AddZero.toZero` `supDegree` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `leadingCoeff`	—	`Zero.instNonempty` `eq_or_ne` `MulZeroClass.zero_mul` `Function.invFun.congr_simp` `supDegree_zero` `MulZeroClass.mul_zero` `exists_supDegree_mem_support` `Function.leftInverse_invFun` `apply_add_of_supDegree_le` `Eq.le`
`exists_supDegree_mem_support` 📖	mathematical	—	`Finset` `Finset.instMembership` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `supDegree` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Finset.exists_mem_eq_sup` `Finsupp.support_nonempty_iff`
`infDegree_withTop_some_comp` 📖	mathematical	`Finset.Nonempty` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`infDegree` `WithTop` `WithTop.semilatticeInf` `WithTop.instOrderTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `WithTop.some`	—	`Finset.coe_inf'` `Finset.inf'_eq_inf`
`le_infDegree_add` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatticeInf.toMin` `infDegree` `AddMonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addAddCommMonoid`	—	`le_inf_support_add`
`le_infDegree_mul` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `infDegree` `DFunLike.coe` `AddHom` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddHom.funLike` `AddMonoidAlgebra` `instMul`	—	`le_inf_support_mul` `Eq.ge` `map_add` `AddHom.addHomClass`
`le_inf_support_add` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatticeInf.toMin` `Finset.inf` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addAddCommMonoid`	—	`sup_support_add_le`
`le_inf_support_finset_prod` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`Finset.sum` `Finset.inf` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finset.prod` `AddMonoidAlgebra` `CommSemiring.toCommMonoid` `commSemiring`	—	`Multiset.map_map` `le_inf_support_multiset_prod`
`le_inf_support_list_prod` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`AddMonoidAlgebra` `Finset.inf` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `zero`	—	`List.Perm.foldr_eq` `instLeftCommutativeOfCommutativeOfAssociative` `instCommutativeMin_mathlib` `instAssociativeMin_mathlib` `OrderDual.ofDual_le_ofDual` `sup_support_list_prod_le` `OrderDual.addLeftMono` `OrderDual.addRightMono`
`le_inf_support_mul` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	`Finset.inf` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `instMul`	—	`sup_support_mul_le` `OrderDual.addLeftMono` `OrderDual.addRightMono`
`le_inf_support_multiset_prod` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`Multiset.sum` `Multiset.map` `AddMonoidAlgebra` `CommSemiring.toSemiring` `Finset.inf` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Multiset.prod` `CommSemiring.toCommMonoid` `commSemiring`	—	`List.Perm.foldr_eq` `instLeftCommutativeOfCommutativeOfAssociative` `instCommutativeMin_mathlib` `instAssociativeMin_mathlib` `OrderDual.ofDual_le_ofDual` `sup_support_multiset_prod_le` `OrderDual.addLeftMono` `OrderDual.addRightMono`
`le_inf_support_pow` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`AddMonoid.toNatSMul` `Finset.inf` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	—	`List.Perm.foldr_eq` `instLeftCommutativeOfCommutativeOfAssociative` `instCommutativeMin_mathlib` `instAssociativeMin_mathlib` `OrderDual.ofDual_le_ofDual` `sup_support_pow_le` `OrderDual.addLeftMono` `OrderDual.addRightMono`
`leadingCoeff_add_eq_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `supDegree` `Lattice.toSemilatticeSup`	`leadingCoeff` `Zero.instNonempty` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `AddZero.toAdd`	—	`Zero.instNonempty` `supDegree_mem_range` `ne_zero_of_not_supDegree_le` `LT.lt.not_ge` `leadingCoeff.eq_1` `supDegree_add_eq_left` `Finsupp.add_apply` `apply_eq_zero_of_not_le_supDegree` `Function.apply_invFun_apply` `add_zero`
`leadingCoeff_add_eq_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `supDegree` `Lattice.toSemilatticeSup`	`leadingCoeff` `Zero.instNonempty` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `AddZero.toAdd`	—	`Zero.instNonempty` `add_comm` `leadingCoeff_add_eq_left`
`leadingCoeff_eq_zero` 📖	mathematical	—	`leadingCoeff` `Zero.instNonempty` `AddZero.toZero` `AddZeroClass.toAddZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `nonUnitalNonAssocSemiring` `AddZero.toAdd`	—	`Zero.instNonempty` `Function.mtr` `leadingCoeff.eq_1` `Finsupp.mem_support_iff` `supDegree_mem_support` `leadingCoeff_zero`
`leadingCoeff_mul` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero`	`leadingCoeff` `Zero.instNonempty` `AddZero.toZero` `AddMonoidAlgebra` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Zero.instNonempty` `eq_or_ne` `leadingCoeff.congr_simp` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `apply_supDegree_add_supDegree` `supDegree_mul` `mul_ne_zero` `leadingCoeff_eq_zero` `leadingCoeff.eq_1`
`leadingCoeff_ne_zero` 📖	—	—	—	—	`Iff.ne` `Zero.instNonempty` `leadingCoeff_eq_zero`
`leadingCoeff_single` 📖	mathematical	—	`leadingCoeff` `single`	—	`leadingCoeff.eq_1` `supDegree_single` `Function.invFun.congr_simp` `Finsupp.single_zero` `Function.leftInverse_invFun` `single_apply`
`leadingCoeff_zero` 📖	mathematical	—	`leadingCoeff` `AddMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`monic_one` 📖	mathematical	—	`Monic` `Zero.instNonempty` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoidAlgebra` `zero`	—	`Zero.instNonempty` `Monic.eq_1` `one_def` `leadingCoeff_single`
`ne_zero_of_not_supDegree_le` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `supDegree`	—	—	`ne_zero_of_supDegree_ne_bot` `bot_le`
`ne_zero_of_supDegree_ne_bot` 📖	—	—	—	—	`supDegree_zero`
`sum_ne_zero_of_injOn_supDegree` 📖	—	`Finset.Nonempty` `Set.InjOn` `AddMonoidAlgebra` `supDegree` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset` `Finset.instSetLike`	—	—	`sum_ne_zero_of_injOn_supDegree'`
`sum_ne_zero_of_injOn_supDegree'` 📖	—	`Finset` `Finset.instMembership` `Set.InjOn` `AddMonoidAlgebra` `supDegree` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SetLike.coe` `Finset.instSetLike`	—	—	`Finset.exists_mem_eq_sup` `Eq.trans_ne` `Finset.sum_eq_single_of_mem` `Mathlib.Tactic.Push.not_forall_eq` `ne_zero_of_supDegree_ne_bot` `LE.le.lt_of_ne` `LE.le.trans_eq` `Finset.le_sup` `Set.InjOn.ne` `Zero.instNonempty` `supDegree_leadingCoeff_sum_eq` `LT.lt.ne_bot`
`supDegree_add_eq_left` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `supDegree` `Lattice.toSemilatticeSup`	`AddMonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	`LE.le.antisymm` `LE.le.trans` `supDegree_add_le` `sup_le` `le_rfl` `LT.lt.le` `exists_supDegree_mem_support` `ne_zero_of_not_supDegree_le` `LT.lt.not_ge` `Finset.le_sup` `Finsupp.mem_support_iff` `Finsupp.add_apply` `apply_eq_zero_of_not_le_supDegree` `add_zero`
`supDegree_add_eq_right` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `supDegree` `Lattice.toSemilatticeSup`	`AddMonoidAlgebra` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `nonUnitalNonAssocSemiring` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	`add_comm` `supDegree_add_eq_left`
`supDegree_add_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `supDegree` `AddMonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addAddCommMonoid` `SemilatticeSup.toMax`	—	`sup_support_add_le`
`supDegree_eq_of_isMaxOn` 📖	mathematical	`Finset` `Finset.instMembership` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsMaxOn` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SetLike.coe` `Finset.instSetLike`	`supDegree`	—	`sup_eq_of_isMaxOn`
`supDegree_eq_of_max` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `Finset` `Finset.instMembership` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Function.invFun` `Zero.instNonempty` `AddZero.toZero` `AddZeroClass.toAddZero` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	`supDegree`	—	`Zero.instNonempty` `sup_eq_of_max`
`supDegree_leadingCoeff_sum_eq` 📖	mathematical	`Finset` `Finset.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `supDegree` `Lattice.toSemilatticeSup`	`Finset.sum` `AddMonoidAlgebra` `addAddCommMonoid` `leadingCoeff` `Zero.instNonempty` `AddZero.toZero` `AddZeroClass.toAddZero`	—	`Zero.instNonempty` `Finset.add_sum_erase` `Finset.sum_empty` `add_zero` `supDegree_sum_lt` `Finset.mem_erase` `supDegree_add_eq_left` `leadingCoeff_add_eq_left`
`supDegree_mem_range` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `supDegree` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`exists_supDegree_mem_support`
`supDegree_mem_support` 📖	mathematical	—	`Finset` `Finset.instMembership` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Function.invFun` `Zero.instNonempty` `AddZero.toZero` `AddZeroClass.toAddZero` `supDegree` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Zero.instNonempty` `exists_supDegree_mem_support` `Function.leftInverse_invFun`
`supDegree_mul` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero`	`supDegree` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidAlgebra` `instMul`	—	`Zero.instNonempty` `supDegree_eq_of_max` `AddSubsemigroup.add_mem` `SetLike.mem_coe` `AddMemClass.add_mem` `AddSubsemigroup.instAddMemClass` `supDegree_mem_range` `apply_supDegree_add_supDegree` `addLeftMono_of_addLeftStrictMono` `addRightMono_of_addRightStrictMono` `LE.le.trans` `Finset.le_sup` `supDegree_mul_le`
`supDegree_mul_le` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `supDegree` `AddMonoidAlgebra` `instMul`	—	`sup_support_mul_le` `Eq.le`
`supDegree_neg` 📖	mathematical	—	`supDegree` `Ring.toSemiring` `AddMonoidAlgebra` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addAddCommGroup`	—	`supDegree.eq_1` `Finsupp.support_neg`
`supDegree_prod_le` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `supDegree` `CommSemiring.toSemiring` `Finset.prod` `AddMonoidAlgebra` `CommSemiring.toCommMonoid` `commSemiring` `Finset.sum`	—	`Finset.induction` `Finset.prod_empty` `Finset.sum_empty` `one_def` `supDegree_single` `bot_le` `Eq.le` `Finset.prod_insert` `Finset.sum_insert` `LE.le.trans` `supDegree_mul_le` `add_le_add_right`
`supDegree_single` 📖	mathematical	—	`supDegree` `single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`Finsupp.single_zero` `instIsEmptyFalse` `supDegree_single_ne_zero`
`supDegree_single_ne_zero` 📖	mathematical	—	`supDegree` `single`	—	`supDegree.eq_1` `Finsupp.support_single_ne_zero` `Finset.sup_singleton`
`supDegree_sub_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `supDegree` `Ring.toSemiring` `AddMonoidAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addAddCommGroup` `SemilatticeSup.toMax`	—	`sub_eq_add_neg` `supDegree_neg` `supDegree_add_le`
`supDegree_sub_lt_of_leadingCoeff_eq` 📖	mathematical	`supDegree` `Ring.toSemiring` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `leadingCoeff` `Zero.instNonempty` `AddZero.toZero` `AddZeroClass.toAddZero`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `AddMonoidAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `nonAssocRing`	—	`Zero.instNonempty` `LE.le.lt_of_ne` `LE.le.trans` `supDegree_sub_le` `sup_idem` `le_refl` `leadingCoeff.eq_1` `leadingCoeff_eq_zero` `sub_eq_zero` `Finsupp.sub_apply`
`supDegree_sum_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `supDegree` `Finset.sum` `AddMonoidAlgebra` `addAddCommMonoid` `Finset.sup`	—	`LE.le.trans_eq` `Finset.sup_mono` `Finsupp.support_finset_sum` `Finset.sup_biUnion`
`supDegree_sum_lt` 📖	mathematical	`Finset.Nonempty` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `supDegree` `Lattice.toSemilatticeSup`	`Finset.sum` `AddMonoidAlgebra` `addAddCommMonoid`	—	`LE.le.trans_lt` `supDegree_sum_le` `Finset.sup_lt_iff` `bot_le`
`supDegree_withBot_some_comp` 📖	mathematical	`Finset.Nonempty` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`supDegree` `WithBot` `WithBot.semilatticeSup` `WithBot.instOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `WithBot.some`	—	`Finset.coe_sup'` `Finset.sup'_eq_sup`
`supDegree_zero` 📖	mathematical	—	`supDegree` `AddMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `nonUnitalNonAssocSemiring` `AddZero.toAdd` `AddZeroClass.toAddZero` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`Finset.sup_empty`
`sup_support_add_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Finset.sup` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `addAddCommMonoid` `SemilatticeSup.toMax`	—	`LE.le.trans_eq` `Finset.sup_mono` `Finsupp.support_add` `Finset.sup_union`
`sup_support_finset_prod_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`Finset.sup` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finset.prod` `AddMonoidAlgebra` `CommSemiring.toCommMonoid` `commSemiring` `Finset.sum`	—	`LE.le.trans_eq` `sup_support_multiset_prod_le` `Multiset.map_map`
`sup_support_list_prod_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`Finset.sup` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `instMul` `zero`	—	`Finset.sup_le_iff` `Finset.mem_singleton` `Finsupp.support_single_subset` `le_imp_le_of_le_of_le` `sup_support_mul_le` `le_refl` `add_le_add_right`
`sup_support_mul_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	`Finset.sup` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `instMul`	—	`le_imp_le_of_le_of_le` `Finset.sup_mono` `support_mul` `le_refl` `Finset.sup_add_le` `add_le_add_left` `Finset.le_sup` `add_le_add_right`
`sup_support_multiset_prod_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`Finset.sup` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Multiset.prod` `AddMonoidAlgebra` `CommSemiring.toCommMonoid` `commSemiring` `Multiset.sum` `Multiset.map`	—	`Multiset.quot_mk_to_coe''` `Multiset.map_coe` `Multiset.sum_coe` `Multiset.prod_coe` `sup_support_list_prod_le`
`sup_support_pow_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`Finset.sup` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `AddMonoid.toNatSMul`	—	`List.prod_replicate` `List.sum_replicate` `LE.le.trans_eq` `sup_support_list_prod_le`

AddMonoidAlgebra.Monic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`leadingCoeff_mul_eq_left` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoidAlgebra.Monic` `Zero.instNonempty` `AddZero.toZero`	`AddMonoidAlgebra.leadingCoeff` `AddMonoidAlgebra` `AddMonoidAlgebra.instMul`	—	`Zero.instNonempty` `eq_or_ne` `MulZeroClass.zero_mul` `AddMonoidAlgebra.leadingCoeff.eq_1` `supDegree_mul_of_ne_zero_left` `AddMonoidAlgebra.apply_supDegree_add_supDegree` `mul_one`
`leadingCoeff_mul_eq_right` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoidAlgebra.Monic` `Zero.instNonempty` `AddZero.toZero`	`AddMonoidAlgebra.leadingCoeff` `AddMonoidAlgebra` `AddMonoidAlgebra.instMul`	—	`Zero.instNonempty` `eq_or_ne` `MulZeroClass.mul_zero` `AddMonoidAlgebra.leadingCoeff.eq_1` `supDegree_mul_of_ne_zero_right` `AddMonoidAlgebra.apply_supDegree_add_supDegree` `one_mul`
`mul` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoidAlgebra.Monic` `Zero.instNonempty` `AddZero.toZero`	`AddMonoidAlgebra` `AddMonoidAlgebra.instMul`	—	`Zero.instNonempty` `eq_1` `leadingCoeff_mul_eq_left`
`ne_zero` 📖	—	`AddMonoidAlgebra.Monic`	—	—	`NeZero.one` `AddMonoidAlgebra.leadingCoeff.congr_simp`
`pow` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidAlgebra.Monic` `Zero.instNonempty` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`AddMonoidAlgebra` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidAlgebra.semiring`	—	`Zero.instNonempty` `pow_zero` `AddMonoidAlgebra.monic_one` `pow_succ'` `mul`
`supDegree_mul` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidAlgebra.Monic` `Zero.instNonempty` `AddZero.toZero`	`AddMonoidAlgebra.supDegree` `Lattice.toSemilatticeSup` `AddMonoidAlgebra` `AddMonoidAlgebra.instMul`	—	`Zero.instNonempty` `subsingleton_or_nontrivial` `Subsingleton.eq_zero` `Unique.instSubsingleton` `MulZeroClass.mul_zero` `AddMonoidAlgebra.supDegree_zero` `supDegree_mul_of_ne_zero_left` `ne_zero`
`supDegree_mul_of_ne_zero_left` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoidAlgebra.Monic` `Zero.instNonempty` `AddZero.toZero`	`AddMonoidAlgebra.supDegree` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidAlgebra` `AddMonoidAlgebra.instMul`	—	`Zero.instNonempty` `subsingleton_or_nontrivial` `Unique.instSubsingleton` `AddMonoidAlgebra.supDegree_mul` `mul_one` `AddMonoidAlgebra.leadingCoeff_eq_zero` `ne_zero`
`supDegree_mul_of_ne_zero_right` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoidAlgebra.Monic` `Zero.instNonempty` `AddZero.toZero`	`AddMonoidAlgebra.supDegree` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidAlgebra` `AddMonoidAlgebra.instMul`	—	`Zero.instNonempty` `subsingleton_or_nontrivial` `Unique.instSubsingleton` `AddMonoidAlgebra.supDegree_mul` `one_mul` `AddMonoidAlgebra.leadingCoeff_eq_zero` `ne_zero`
`supDegree_pow` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidAlgebra.Monic` `Zero.instNonempty`	`AddMonoidAlgebra.supDegree` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidAlgebra` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidAlgebra.semiring` `AddMonoid.toNatSMul`	—	`Zero.instNonempty` `pow_zero` `zero_nsmul` `AddMonoidAlgebra.one_def` `AddMonoidAlgebra.supDegree_single` `one_ne_zero` `NeZero.one` `pow_succ'` `supDegree_mul_of_ne_zero_left` `pow` `ne_zero` `succ_nsmul'`

---

← Back to Index