Documentation Verification Report

ComputeDegree

📁 Source: Mathlib/Tactic/ComputeDegree.lean

Statistics

Metric	Count
Definitions `computeDegree`, `dispatchLemma`, `getCongrLemma`, `miscomputedDegree?`, `monicityMacro`, `splitApply`, `tacticCompute_degree!`, `tacticMonicity!`, `try_rfl`, `twoHeadsArgs`	10
Theorems `coeff_add_of_eq`, `coeff_congr`, `coeff_congr_lhs`, `coeff_intCast_ite`, `coeff_mul_add_of_le_natDegree_of_eq_ite`, `coeff_pow_of_natDegree_le_of_eq_ite'`, `coeff_smul`, `coeff_sub_of_eq`, `degree_eq_of_le_of_coeff_ne_zero'`, `degree_smul_le_of_le`, `natDegree_C_le`, `natDegree_eq_of_le_of_coeff_ne_zero'`, `natDegree_intCast_le`, `natDegree_natCast_le`, `natDegree_one_le`, `natDegree_smul_le_of_le`, `natDegree_zero_le`	17
Total	27

Mathlib.Tactic.ComputeDegree

Definitions

Name	Category	Theorems
`computeDegree` 📖	CompOp	—
`dispatchLemma` 📖	CompOp	—
`getCongrLemma` 📖	CompOp	—
`miscomputedDegree?` 📖	CompOp	—
`monicityMacro` 📖	CompOp	—
`splitApply` 📖	CompOp	—
`tacticCompute_degree!` 📖	CompOp	—
`tacticMonicity!` 📖	CompOp	—
`try_rfl` 📖	CompOp	—
`twoHeadsArgs` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_add_of_eq` 📖	mathematical	`Polynomial.coeff`	`Polynomial` `Polynomial.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Polynomial.coeff_add`
`coeff_congr` 📖	—	`Polynomial.coeff`	—	—	—
`coeff_congr_lhs` 📖	—	`Polynomial.coeff`	—	—	—
`coeff_intCast_ite` 📖	mathematical	—	`Polynomial.coeff` `Ring.toSemiring` `Polynomial` `Polynomial.instIntCast` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`Polynomial.coeff_C` `Int.cast_ite` `Int.cast_zero`
`coeff_mul_add_of_le_natDegree_of_eq_ite` 📖	mathematical	`Polynomial.natDegree` `Polynomial.coeff`	`Polynomial` `Polynomial.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Polynomial.coeff_mul_add_eq_of_natDegree_le` `Polynomial.coeff_eq_zero_of_natDegree_lt` `lt_of_le_of_lt` `Polynomial.natDegree_mul_le_of_le` `lt_of_le_of_ne`
`coeff_pow_of_natDegree_le_of_eq_ite'` 📖	mathematical	`Polynomial.natDegree` `Polynomial.coeff`	`Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Polynomial.coeff_pow_of_natDegree_le` `Polynomial.coeff_eq_zero_of_natDegree_lt` `lt_of_le_of_lt` `Polynomial.natDegree_pow_le_of_le` `lt_of_le_of_ne`
`coeff_smul` 📖	mathematical	—	`Polynomial.coeff` `Polynomial` `SMulZeroClass.toSMul` `Polynomial.instZero` `Polynomial.smulZeroClass` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`coeff_sub_of_eq` 📖	mathematical	`Polynomial.coeff` `Ring.toSemiring`	`Polynomial` `Polynomial.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`Polynomial.coeff_sub`
`degree_eq_of_le_of_coeff_ne_zero'` 📖	—	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `Polynomial.coeff` `WithBot.unbotD`	—	—	`eq_or_ne` `bot_unique` `WithBot.ne_bot_iff_exists` `Polynomial.degree_eq_of_le_of_coeff_ne_zero`
`degree_smul_le_of_le` 📖	mathematical	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne`	`Polynomial` `SMulZeroClass.toSMul` `Polynomial.instZero` `Polynomial.smulZeroClass`	—	`LE.le.trans` `Polynomial.degree_smul_le`
`natDegree_C_le` 📖	mathematical	—	`Polynomial.natDegree` `DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C`	—	`Eq.le` `Polynomial.natDegree_C`
`natDegree_eq_of_le_of_coeff_ne_zero'` 📖	—	`Polynomial.natDegree` `Polynomial.coeff`	—	—	`Polynomial.natDegree_eq_of_le_of_coeff_ne_zero`
`natDegree_intCast_le` 📖	mathematical	—	`Polynomial.natDegree` `Ring.toSemiring` `Polynomial` `Polynomial.instIntCast`	—	`Eq.le` `Polynomial.natDegree_intCast`
`natDegree_natCast_le` 📖	mathematical	—	`Polynomial.natDegree` `Polynomial` `Polynomial.instNatCast`	—	`Eq.le` `Polynomial.natDegree_natCast`
`natDegree_one_le` 📖	mathematical	—	`Polynomial.natDegree` `Polynomial` `Polynomial.instOne`	—	`Eq.le` `Polynomial.natDegree_one`
`natDegree_smul_le_of_le` 📖	mathematical	`Polynomial.natDegree`	`Polynomial` `SMulZeroClass.toSMul` `Polynomial.instZero` `Polynomial.smulZeroClass`	—	`LE.le.trans` `Polynomial.natDegree_smul_le`
`natDegree_zero_le` 📖	mathematical	—	`Polynomial.natDegree` `Polynomial` `Polynomial.instZero`	—	`Eq.le` `Polynomial.natDegree_zero`

---

← Back to Index