Documentation Verification Report

NoZeroDivisors

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

Statistics

Metric	Count
Definitions	0
Theorems `degreeOf_C_mul`, `degreeOf_mul_eq`, `degreeOf_pow_eq`, `degreeOf_prod_eq`, `degrees_mul_eq`, `dvd_C_iff_exists`, `dvd_X_iff_exists`, `dvd_monomial_iff_exists`, `dvd_monomial_one_iff_exists`, `dvd_smul_X_iff_exists`, `totalDegree_le_of_dvd_of_isDomain`, `totalDegree_mul_of_isDomain`	12
Total	12

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`degreeOf_C_mul` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	`degreeOf` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `commSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `C`	—	`MulZeroClass.mul_zero` `degreeOf_zero` `degreeOf_eq_natDegree` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Polynomial.natDegree_mul'` `rename_injective` `Equiv.injective` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `EquivLike.toEmbeddingLike` `algHom_C` `optionEquivLeft_C` `Polynomial.leadingCoeff_C` `Mathlib.Tactic.Contrapose.contrapose₄` `ext` `coeff_C_mul` `Polynomial.natDegree_C` `natDegree_optionEquivLeft` `zero_add`
`degreeOf_mul_eq` 📖	mathematical	—	`degreeOf` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`degreeOf_eq_natDegree` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Polynomial.natDegree_mul` `instNoZeroDivisors` `EquivLike.toEmbeddingLike` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass`
`degreeOf_pow_eq` 📖	mathematical	—	`degreeOf` `MvPolynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `commSemiring`	—	`Finset.pow_eq_prod_const` `degreeOf_prod_eq` `Finset.sum_const` `Finset.card_range`
`degreeOf_prod_eq` 📖	mathematical	—	`degreeOf` `Finset.prod` `MvPolynomial` `CommSemiring.toCommMonoid` `commSemiring` `Finset.sum` `Nat.instAddCommMonoid`	—	`subsingleton_or_nontrivial` `Finset.prod_congr` `Subsingleton.eq_zero` `degreeOf_zero` `Finset.sum_congr` `Finset.sum_const_zero` `Finset.induction_on` `degreeOf_one` `Finset.prod_insert` `degreeOf_mul_eq` `Finset.prod_ne_zero_iff` `instNoZeroDivisors` `Finset.sum_insert`
`degrees_mul_eq` 📖	mathematical	—	`degrees` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring` `Multiset` `Multiset.instAdd`	—	`Multiset.ext'` `Multiset.count_add` `degreeOf_mul_eq`
`dvd_C_iff_exists` 📖	mathematical	—	`MvPolynomial` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `commSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `C`	—	`Nat.instCanonicallyOrderedAdd` `totalDegree_C` `totalDegree_le_of_dvd_of_isDomain` `coeff_zero_C` `C_dvd_iff_dvd_coeff` `totalDegree_eq_zero_iff_eq_C` `map_dvd` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass`
`dvd_X_iff_exists` 📖	mathematical	—	`MvPolynomial` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `instCommRingMvPolynomial` `X` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `commSemiring` `RingHom.instFunLike` `C` `Algebra.toSMul` `algebra` `Algebra.id`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Unique.instSubsingleton` `Zero.instNonempty` `one_smul` `dvd_smul_X_iff_exists` `one_ne_zero'` `NeZero.one` `isUnit_iff_dvd_one`
`dvd_monomial_iff_exists` 📖	mathematical	—	`MvPolynomial` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `instCommRingMvPolynomial` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `commSemiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instLE`	—	`mul_comm` `C_mul_monomial` `mul_one` `dvd_monomial_mul_iff_exists` `NoZeroDivisors.to_isCancelMulZero` `dvd_C_iff_exists` `map_dvd` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass`
`dvd_monomial_one_iff_exists` 📖	mathematical	—	`MvPolynomial` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `instCommRingMvPolynomial` `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` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`subsingleton_or_nontrivial` `le_refl` `Unique.instSubsingleton` `dvd_monomial_iff_exists` `one_ne_zero'` `NeZero.one`
`dvd_smul_X_iff_exists` 📖	mathematical	—	`MvPolynomial` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `instCommRingMvPolynomial` `Algebra.toSMul` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`X.eq_1` `smul_monomial` `smul_eq_mul` `mul_one` `dvd_monomial_iff_exists` `Finsupp.ext` `le_refl` `LE.le.trans` `Eq.le` `Finsupp.single_eq_of_ne` `le_antisymm` `Finsupp.single_eq_same` `Nat.instCanonicallyOrderedAdd` `Finsupp.instCanonicallyOrderedAddOfAddLeftMono` `Nat.instOrderedSub` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `le_rfl`
`totalDegree_le_of_dvd_of_isDomain` 📖	mathematical	`MvPolynomial` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `commSemiring`	`totalDegree`	—	`totalDegree_mul_of_isDomain` `instNoZeroDivisors`
`totalDegree_mul_of_isDomain` 📖	mathematical	—	`totalDegree` `MvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commSemiring`	—	`exists_wellOrder` `IsWellOrder.toIsWellFounded` `isWellOrder_gt` `instWellFoundedGTOrderDualOfWellFoundedLT` `degree_degLexDegree` `MonomialOrder.degree_mul` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass`

---

← Back to Index