Documentation Verification Report

CancelLeads

📁 Source: Mathlib/Algebra/Polynomial/CancelLeads.lean

Statistics

Metric	Count
Definitions `cancelLeads`	1
Theorems `dvd_cancelLeads_of_dvd_of_dvd`, `natDegree_cancelLeads_lt_of_natDegree_le_natDegree`, `natDegree_cancelLeads_lt_of_natDegree_le_natDegree_of_comm`, `neg_cancelLeads`	4
Total	5

Polynomial

Definitions

Name	Category	Theorems
`cancelLeads` 📖	CompOp	4 math math: `neg_cancelLeads`, `natDegree_cancelLeads_lt_of_natDegree_le_natDegree`, `natDegree_cancelLeads_lt_of_natDegree_le_natDegree_of_comm`, `dvd_cancelLeads_of_dvd_of_dvd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_cancelLeads_of_dvd_of_dvd` 📖	mathematical	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `commRing`	`cancelLeads` `CommRing.toRing`	—	`dvd_sub` `Dvd.dvd.trans` `Dvd.intro_left`
`natDegree_cancelLeads_lt_of_natDegree_le_natDegree` 📖	mathematical	`natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Ring.toSemiring` `CommRing.toRing` `cancelLeads`	—	`natDegree_cancelLeads_lt_of_natDegree_le_natDegree_of_comm` `mul_comm`
`natDegree_cancelLeads_lt_of_natDegree_le_natDegree_of_comm` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `leadingCoeff` `Ring.toSemiring` `natDegree`	`cancelLeads`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `mul_one` `MulZeroClass.zero_mul` `tsub_zero` `MulZeroClass.mul_zero` `sub_self` `cancelLeads.eq_1` `sub_eq_add_neg` `tsub_eq_zero_iff_le` `LE.le.trans_lt` `le_of_eq` `lt_of_le_of_ne` `le_trans` `natDegree_add_le_of_le` `natDegree_mul_le_of_le` `Mathlib.Tactic.ComputeDegree.natDegree_C_le` `le_rfl` `natDegree_neg_le_of_le` `natDegree_pow_le_of_le` `natDegree_X_le` `zero_add` `le_refl` `Mathlib.Tactic.Contrapose.contrapose₄` `leadingCoeff_eq_zero` `leadingCoeff.eq_1` `mul_assoc` `X_pow_mul` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `add_comm` `add_tsub_cancel_left` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `coeff_add` `coeff_C_mul` `coeff_neg` `coeff_mul_X_pow` `add_neg_cancel`
`neg_cancelLeads` 📖	mathematical	—	`Polynomial` `Ring.toSemiring` `instNeg` `cancelLeads`	—	`neg_sub`

---

← Back to Index