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 AddMonoidAlgebra.zero Finsupp CommSemiring.toSemiring Finsupp.instZero	—	divMonomial_monomial
X_dvd_X 📖	mathematical	—	MvPolynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero AddMonoidAlgebra.nonUnitalSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring AddMonoid.toAddSemigroup Finsupp.instAddMonoid Nat.instAddMonoid X	—	monomial_one_dvd_monomial_one Nat.instCanonicallyOrderedAdd
X_dvd_iff_modMonomial_eq_zero 📖	mathematical	—	MvPolynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero AddMonoidAlgebra.nonUnitalSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring AddMonoid.toAddSemigroup Finsupp.instAddMonoid Nat.instAddMonoid X modMonomial Finsupp.single NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp.instAdd AddMonoid.toAddZeroClass	—	monomial_one_dvd_iff_modMonomial_eq_zero
X_dvd_monomial 📖	mathematical	—	MvPolynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero AddMonoidAlgebra.nonUnitalSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring AddMonoid.toAddSemigroup Finsupp.instAddMonoid Nat.instAddMonoid X DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike monomial NonUnitalNonAssocSemiring.toMulZeroClass	—	monomial_dvd_monomial Nat.instCanonicallyOrderedAdd
X_dvd_mul_iff 📖	mathematical	—	MvPolynomial CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero AddMonoidAlgebra.nonUnitalSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring AddMonoid.toAddSemigroup Finsupp.instAddMonoid Nat.instAddMonoid X AddMonoidAlgebra.instMul Finsupp.instAdd AddMonoid.toAddZeroClass	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton IsLeftCancelMulZero.to_noZeroDivisors AddMonoidAlgebra.instIsLeftCancelAddZeroOfIsCancelAddOfUniqueSums AddCancelMonoid.toIsCancelAdd IsCancelMulZero.toIsLeftCancelMulZero instUniqueSumsFinsupp TwoUniqueSums.toUniqueSums TwoUniqueSums.of_covariant_left instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add 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 AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid X Finsupp.single	—	divMonomial_monomial_mul
X_mul_modMonomial 📖	mathematical	—	modMonomial MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid X Finsupp.single NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring	—	monomial_mul_modMonomial
X_prime 📖	mathematical	—	Prime MvPolynomial CommRing.toCommSemiring CommSemiring.toCommMonoidWithZero AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid 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 AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid	—	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 MulZeroClass.toZero 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 AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidAlgebra.instMul DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.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 AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidAlgebra.instMul X divMonomial Finsupp.single modMonomial	—	divMonomial_add_modMonomial
divMonomial_monomial 📖	mathematical	—	divMonomial DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddMonoidAlgebra.zero Finsupp.instZero	—	AddMonoidAlgebra.of'_divOf
divMonomial_monomial_mul 📖	mathematical	—	divMonomial MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.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 AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.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 AddMonoidAlgebra.nonUnitalSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring AddMonoid.toAddSemigroup Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.instMul Finsupp.instAdd AddMonoid.toAddZeroClass X divMonomial Finsupp.single	—	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 AddMonoidAlgebra.nonUnitalSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring AddMonoid.toAddSemigroup Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.instMul Finsupp.instAdd AddMonoid.toAddZeroClass DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add 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 IsOrderedCancelAddMonoid.toAddLeftReflectLT Finsupp.isOrderedCancelAddMonoid 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 AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidAlgebra.instMul X DFunLike.coe Finsupp.instFunLike	divMonomial Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass	—	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 AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidAlgebra.instMul X DFunLike.coe Finsupp.instFunLike	modMonomial Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass	—	IsCancelAdd.toIsLeftCancelAdd instIsCancelAddOfIsLeftCancelAdd eq_divMonomial_single divMonomial_add_modMonomial_single
eq_modMonomial_single_iff 📖	mathematical	MvPolynomial CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero AddMonoidAlgebra.nonUnitalSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring AddMonoid.toAddSemigroup Finsupp.instAddMonoid Nat.instAddMonoid X SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidAlgebra.ring CommRing.toRing	modMonomial CommRing.toCommSemiring 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 AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid	—	ext coeff_add AddCommMagma.IsLeftCancelAdd.toIsCancelAdd
modMonomial_X 📖	mathematical	—	modMonomial X Finsupp.single MulZeroClass.toZero Nat.instMulZeroClass MvPolynomial NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid	—	monomial_modMonomial
modMonomial_add_divMonomial 📖	mathematical	—	MvPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid modMonomial AddMonoidAlgebra.instMul DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.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 AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid modMonomial Finsupp.single AddMonoidAlgebra.instMul X divMonomial	—	modMonomial_add_divMonomial
monomial_dvd_monomial 📖	mathematical	—	MvPolynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero AddMonoidAlgebra.nonUnitalSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring AddMonoid.toAddSemigroup Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike monomial NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instLE NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring	—	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 AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid	—	AddMonoidAlgebra.of'_modOf
monomial_mul_modMonomial 📖	mathematical	—	modMonomial MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring	—	AddMonoidAlgebra.of'_mul_modOf
monomial_one_dvd_iff_modMonomial_eq_zero 📖	mathematical	—	MvPolynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero AddMonoidAlgebra.nonUnitalSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring AddMonoid.toAddSemigroup Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne modMonomial NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp.instAdd AddMonoid.toAddZeroClass	—	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 AddMonoidAlgebra.nonUnitalSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring AddMonoid.toAddSemigroup Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finsupp.instLE	—	monomial_dvd_monomial NeZero.one
mul_X_divMonomial 📖	mathematical	—	divMonomial MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid X Finsupp.single	—	divMonomial_mul_monomial
mul_X_modMonomial 📖	mathematical	—	modMonomial MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid X Finsupp.single NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring	—	mul_monomial_modMonomial
mul_monomial_modMonomial 📖	mathematical	—	modMonomial MvPolynomial AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.addAddCommMonoid Semiring.toModule AddMonoidAlgebra.module LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring	—	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 instIsLeftCancelAddOfAddLeftReflectLE AddZero.toAdd AddZeroClass.toAddZero Nat.instPartialOrder IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instAddCommMonoid Nat.instPreorder Nat.instIsOrderedCancelAddMonoid Set.preimage SetLike.coe Finset Finset.instSetLike	—	—
zero_divMonomial 📖	mathematical	—	divMonomial MvPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid	—	AddMonoidAlgebra.zero_divOf

---

← Back to Index