Groebner

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

Statistics

Metric	Count
Definitions reduce, subLTerm	2
Theorems degree_reduce_lt, degree_sub_LTerm_le, degree_sub_LTerm_lt, div, div_set, div_single	6
Total	8

MonomialOrder

Definitions

Name	Category	Theorems
reduce 📖	CompOp	1 math math: degree_reduce_lt
subLTerm 📖	CompOp	2 math math: degree_sub_LTerm_lt, degree_sub_LTerm_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
degree_reduce_lt 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring leadingCoeff Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instLE degree	syn Preorder.toLT 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 reduce	—	Nat.instCanonicallyOrderedAdd Nat.instOrderedSub degree_monomial degree_zero Finsupp.ext tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Finsupp.instCanonicallyOrderedAddOfAddLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Finsupp.isOrderedAddMonoid Finsupp.orderedSub MvPolynomial.coeff_sub coeff_mul_of_degree_add leadingCoeff_monomial mul_comm mul_assoc IsUnit.mul_val_inv one_mul leadingCoeff.eq_1 lt_iff_le_and_ne le_trans degree_sub_le degree_mul_le AddEquiv.injective leadingCoeff_eq_zero_iff EquivLike.toEmbeddingLike
degree_sub_LTerm_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 subLTerm	—	le_trans degree_sub_le degree_monomial_le
degree_sub_LTerm_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 subLTerm	—	lt_iff_le_and_ne degree_sub_LTerm_le degree_zero EquivLike.toEmbeddingLike coeff_degree_ne_zero_iff MvPolynomial.coeff_sub MvPolynomial.coeff_monomial sub_self
div 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring leadingCoeff	MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial DFunLike.coe LinearMap MvPolynomial.commSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Finsupp.linearCombination syn Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder lo AddEquiv Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup acm EquivLike.toFunLike AddEquiv.instEquivLike toSyn degree Distrib.toMul Finsupp.instFunLike Finsupp.instLE	—	isWellFounded_iff wf Finsupp.linearCombination_single add_zero smul_mul_assoc Units.instIsScalarTower IsScalarTower.right eq_C_of_degree_eq_zero mul_comm MvPolynomial.smul_eq_C_mul le_trans degree_mul_le Finsupp.single_eq_same zero_add le_of_eq EquivLike.toEmbeddingLike degree_smul_of_isRegular Units.isRegular Finsupp.single_eq_of_ne MulZeroClass.mul_zero degree_zero map_zero AddMonoidHomClass.toZeroHomClass AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass bot_le instIsEmptyFalse DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass degree_reduce_lt Finsupp.instCanonicallyOrderedAddOfAddLeftMono Nat.instCanonicallyOrderedAdd Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid map_add SemilinearMapClass.toAddHomClass add_assoc add_comm sub_add_cancel mul_add Distrib.leftDistribClass degree_add_le le_of_lt Finsupp.single_apply le_imp_le_of_le_of_le le_refl AddMonoidHomClass.toAddHomClass add_le_add_right IsOrderedCancelAddMonoid.toIsOrderedAddMonoid iocam degree_monomial_le add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Finsupp.isOrderedAddMonoid Finsupp.orderedSub degree_sub_LTerm_lt sub_eq_zero degree_sub_LTerm_le MvPolynomial.support_add MvPolynomial.support_monomial_subset Finset.mem_union
div_set 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring leadingCoeff	MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial DFunLike.coe LinearMap MvPolynomial.commSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp Set.Elem MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Finsupp.linearCombination Set Set.instMembership syn Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder lo AddEquiv Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup acm EquivLike.toFunLike AddEquiv.instEquivLike toSyn degree Distrib.toMul Finsupp.instFunLike Finsupp.instLE	—	div Subtype.prop
div_single 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring leadingCoeff	MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial Distrib.toMul 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 Finsupp.instLE	—	div_set AddRightCancelSemigroup.toIsRightCancelAdd Finsupp.sum_eq_single instIsEmptyFalse MulZeroClass.zero_mul

---

← Back to Index