Division

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

Statistics

Metric	Count
Definitions divMonomial, modMonomial	2
Theorems X_divMonomial, X_dvd_X, X_dvd_iff_modMonomial_eq_zero, X_dvd_monomial, X_dvd_mul_iff, X_mul_divMonomial, X_mul_modMonomial, X_prime, add_divMonomial, coeff_divMonomial, coeff_modMonomial_of_le, coeff_modMonomial_of_not_le, divMonomial_add, divMonomial_add_modMonomial, divMonomial_add_modMonomial_single, divMonomial_monomial, divMonomial_monomial_mul, divMonomial_mul_monomial, divMonomial_zero, dvd_X_mul_iff, dvd_monomial_mul_iff_exists, eq_divMonomial_single, eq_modMonomial_single, eq_modMonomial_single_iff, instIsCancelAddOfIsLeftCancelAdd, modMonomial_X, modMonomial_add_divMonomial, modMonomial_add_divMonomial_single, monomial_dvd_monomial, monomial_modMonomial, monomial_mul_modMonomial, monomial_one_dvd_iff_modMonomial_eq_zero, monomial_one_dvd_monomial_one, mul_X_divMonomial, mul_X_modMonomial, mul_monomial_modMonomial, support_divMonomial, zero_divMonomial	38
Total	40

MvPolynomial

Definitions

Name	Category	Theorems
divMonomial 📖	CompOp	18 math math: mul_X_divMonomial, zero_divMonomial, coeff_divMonomial, divMonomial_add_modMonomial, eq_divMonomial_single, modMonomial_add_divMonomial, dvd_X_mul_iff, divMonomial_mul_monomial, divMonomial_monomial, X_mul_divMonomial, add_divMonomial, support_divMonomial, divMonomial_monomial_mul, divMonomial_zero, divMonomial_add_modMonomial_single, modMonomial_add_divMonomial_single, X_divMonomial, divMonomial_add
modMonomial 📖	CompOp	16 math math: divMonomial_add_modMonomial, monomial_one_dvd_iff_modMonomial_eq_zero, eq_modMonomial_single_iff, coeff_modMonomial_of_le, modMonomial_add_divMonomial, eq_modMonomial_single, modMonomial_X, X_dvd_iff_modMonomial_eq_zero, X_mul_modMonomial, coeff_modMonomial_of_not_le, divMonomial_add_modMonomial_single, mul_monomial_modMonomial, mul_X_modMonomial, modMonomial_add_divMonomial_single, monomial_modMonomial, monomial_mul_modMonomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
X_divMonomial 📖	mathematical	—	divMonomial X Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass MvPolynomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring	—	divMonomial_monomial
X_dvd_X 📖	mathematical	—	MvPolynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring commSemiring X	—	monomial_one_dvd_monomial_one Nat.instCanonicallyOrderedAdd
X_dvd_iff_modMonomial_eq_zero 📖	mathematical	—	MvPolynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring commSemiring X modMonomial Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	monomial_one_dvd_iff_modMonomial_eq_zero
X_dvd_monomial 📖	mathematical	—	MvPolynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring commSemiring X DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	monomial_dvd_monomial Nat.instCanonicallyOrderedAdd
X_dvd_mul_iff 📖	mathematical	—	MvPolynomial CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing instCommRingMvPolynomial X Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton IsLeftCancelMulZero.to_noZeroDivisors IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZeroOfIsCancelAdd AddCancelMonoid.toIsCancelAdd modMonomial_add_divMonomial_single eq_modMonomial_single_iff mul_add Distrib.leftDistribClass add_mul Distrib.rightDistribClass add_assoc add_sub_cancel_left mul_comm mul_assoc dvd_mul_right Mathlib.Tactic.Contrapose.contrapose₁ notMem_support_iff coeff_mul Finset.sum_eq_zero coeff_modMonomial_of_le Nat.instCanonicallyOrderedAdd MulZeroClass.zero_mul mul_eq_zero dvd_mul_of_dvd_left dvd_mul_of_dvd_right
X_mul_divMonomial 📖	mathematical	—	divMonomial MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring X Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass	—	divMonomial_monomial_mul
X_mul_modMonomial 📖	mathematical	—	modMonomial MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring X Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toMulZeroClass	—	monomial_mul_modMonomial
X_prime 📖	mathematical	—	Prime MvPolynomial CommRing.toCommSemiring CommSemiring.toCommMonoidWithZero commSemiring X	—	X_ne_zero isUnit_iff_exists map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass constantCoeff_X MulZeroClass.zero_mul map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass NeZero.one X_dvd_mul_iff
add_divMonomial 📖	mathematical	—	divMonomial MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring	—	map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass
coeff_divMonomial 📖	mathematical	—	coeff divMonomial Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid	—	—
coeff_modMonomial_of_le 📖	mathematical	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instLE	coeff modMonomial NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	AddMonoidAlgebra.modOf_apply_of_exists_add ExistsAddOfLE.exists_add_of_le CanonicallyOrderedAdd.toExistsAddOfLE Finsupp.instCanonicallyOrderedAddOfAddLeftMono Nat.instCanonicallyOrderedAdd Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
coeff_modMonomial_of_not_le 📖	mathematical	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instLE	coeff modMonomial	—	AddMonoidAlgebra.modOf_apply_of_not_exists_add le_self_add Finsupp.instCanonicallyOrderedAddOfAddLeftMono Nat.instCanonicallyOrderedAdd Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
divMonomial_add 📖	mathematical	—	divMonomial Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid	—	AddMonoidAlgebra.divOf_add Finsupp.instIsCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd Nat.instIsOrderedCancelAddMonoid
divMonomial_add_modMonomial 📖	mathematical	—	MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Distrib.toMul DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne divMonomial modMonomial	—	AddMonoidAlgebra.divOf_add_modOf Finsupp.instIsCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd Nat.instIsOrderedCancelAddMonoid
divMonomial_add_modMonomial_single 📖	mathematical	—	MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Distrib.toMul X divMonomial Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass modMonomial	—	divMonomial_add_modMonomial
divMonomial_monomial 📖	mathematical	—	divMonomial DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	AddMonoidAlgebra.of'_divOf
divMonomial_monomial_mul 📖	mathematical	—	divMonomial MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	AddMonoidAlgebra.of'_mul_divOf Finsupp.instIsCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd Nat.instIsOrderedCancelAddMonoid
divMonomial_mul_monomial 📖	mathematical	—	divMonomial MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	AddMonoidAlgebra.mul_of'_divOf Finsupp.instIsCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd Nat.instIsOrderedCancelAddMonoid
divMonomial_zero 📖	mathematical	—	divMonomial Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero	—	AddMonoidAlgebra.divOf_zero Finsupp.instIsCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd Nat.instIsOrderedCancelAddMonoid
dvd_X_mul_iff 📖	mathematical	—	MvPolynomial CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing instCommRingMvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing X divMonomial Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass	—	dvd_mul_right X_mul_cancel_left_iff mul_left_comm mul_assoc zero_add X_dvd_iff_modMonomial_eq_zero modMonomial_add_divMonomial_single dvd_mul_of_dvd_right modMonomial_add_divMonomial one_mul AddRightCancelSemigroup.toIsRightCancelAdd mul_dvd_mul_left
dvd_monomial_mul_iff_exists 📖	mathematical	—	MvPolynomial CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing instCommRingMvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instLE	—	subsingleton_or_nontrivial Unique.instSubsingleton le_refl Finsupp.degree_eq_zero_iff Nat.instCanonicallyOrderedAdd one_mul Finsupp.instCanonicallyOrderedAddOfAddLeftMono Nat.instOrderedSub IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Finsupp.support_nonempty_iff map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass Finsupp.sub_add_single_one_cancel Finsupp.mem_support_iff Finsupp.isOrderedAddMonoid Finsupp.addLeftReflectLE IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le AddRightCancelSemigroup.toIsRightCancelAdd map_add AddMonoidHomClass.toAddHomClass Finsupp.degree_single dvd_X_mul_iff mul_assoc mul_comm pow_one monomial_add_single le_trans covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT Finsupp.instIsRightCancelAdd contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLT Finsupp.isOrderedCancelAddMonoid Nat.instIsOrderedCancelAddMonoid X_mul_divMonomial add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Finsupp.orderedSub mul_one monomial_mul mul_dvd_mul dvd_rfl dvd_mul_of_dvd_right
eq_divMonomial_single 📖	mathematical	MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Distrib.toMul X DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instFunLike	divMonomial Finsupp.single	—	ext coeff_divMonomial coeff_add coeff_X_mul left_eq_add notMem_support_iff Finsupp.single_eq_same
eq_modMonomial_single 📖	mathematical	MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Distrib.toMul X DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instFunLike	modMonomial Finsupp.single	—	IsCancelAdd.toIsLeftCancelAdd instIsCancelAddOfIsLeftCancelAdd eq_divMonomial_single divMonomial_add_modMonomial_single
eq_modMonomial_single_iff 📖	mathematical	MvPolynomial CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing instCommRingMvPolynomial X SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	modMonomial Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass DFunLike.coe Finsupp Finsupp.instFunLike	—	Mathlib.Tactic.Contrapose.contrapose₁ notMem_support_iff coeff_modMonomial_of_le Nat.instCanonicallyOrderedAdd eq_modMonomial_single AddLeftCancelSemigroup.toIsLeftCancelAdd sub_eq_iff_eq_add
instIsCancelAddOfIsLeftCancelAdd 📖	mathematical	—	IsCancelAdd MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring	—	ext coeff_add AddCommMagma.IsLeftCancelAdd.toIsCancelAdd
modMonomial_X 📖	mathematical	—	modMonomial X Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass MvPolynomial NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring	—	monomial_modMonomial
modMonomial_add_divMonomial 📖	mathematical	—	MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring modMonomial Distrib.toMul DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne divMonomial	—	AddMonoidAlgebra.modOf_add_divOf Finsupp.instIsCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd Nat.instIsOrderedCancelAddMonoid
modMonomial_add_divMonomial_single 📖	mathematical	—	MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring modMonomial Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass Distrib.toMul X divMonomial	—	modMonomial_add_divMonomial
monomial_dvd_monomial 📖	mathematical	—	MvPolynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring commSemiring DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp Nat.instMulZeroClass Finsupp.instLE	—	ext_iff Nat.instCanonicallyOrderedAdd Nat.instOrderedSub coeff_monomial_mul' coeff_monomial dvd_zero monomial_zero monomial_mul add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Finsupp.instCanonicallyOrderedAddOfAddLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Finsupp.isOrderedAddMonoid Finsupp.orderedSub
monomial_modMonomial 📖	mathematical	—	modMonomial DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring Semiring.toModule module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	AddMonoidAlgebra.of'_modOf
monomial_mul_modMonomial 📖	mathematical	—	modMonomial MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	AddMonoidAlgebra.of'_mul_modOf
monomial_one_dvd_iff_modMonomial_eq_zero 📖	mathematical	—	MvPolynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring commSemiring DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne modMonomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	AddMonoidAlgebra.of'_dvd_iff_modOf_eq_zero Finsupp.instIsCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd Nat.instIsOrderedCancelAddMonoid
monomial_one_dvd_monomial_one 📖	mathematical	—	MvPolynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring commSemiring DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instLE	—	monomial_dvd_monomial NeZero.one
mul_X_divMonomial 📖	mathematical	—	divMonomial MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring X Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass	—	divMonomial_mul_monomial
mul_X_modMonomial 📖	mathematical	—	modMonomial MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring X Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toMulZeroClass	—	mul_monomial_modMonomial
mul_monomial_modMonomial 📖	mathematical	—	modMonomial MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	AddMonoidAlgebra.mul_of'_modOf
support_divMonomial 📖	mathematical	—	support divMonomial Finset.preimage Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid Function.Injective.injOn add_right_injective Finsupp.instIsLeftCancelAdd AddLeftCancelSemigroup.toIsLeftCancelAdd AddLeftCancelMonoid.toAddLeftCancelSemigroup AddCancelCommMonoid.toAddLeftCancelMonoid Nat.instAddCancelCommMonoid Set.preimage SetLike.coe Finset Finset.instSetLike	—	—
zero_divMonomial 📖	mathematical	—	divMonomial MvPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring	—	AddMonoidAlgebra.zero_divOf

---

← Back to Index