Documentation Verification Report

CoeffList

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

Statistics

Metric	Count
Definitions `coeffList`	1
Theorems `coeffList_C`, `coeffList_C_mul`, `coeffList_eq_cons_leadingCoeff`, `coeffList_eq_nil`, `coeffList_eraseLead`, `coeffList_monomial`, `coeffList_neg`, `coeffList_zero`, `head?_coeffList`, `head_coeffList`, `leadingCoeff_cons_eraseLead`, `length_coeffList_eq_ite`, `length_coeffList_eq_withBotSucc_degree`	13
Total	14

Polynomial

Definitions

Name	Category	Theorems
`coeffList` 📖	CompOp	13 math math: `coeffList_eq_cons_leadingCoeff`, `coeffList_C_mul`, `length_coeffList_eq_withBotSucc_degree`, `length_coeffList_eq_ite`, `leadingCoeff_cons_eraseLead`, `coeffList_eraseLead`, `head_coeffList`, `coeffList_C`, `coeffList_eq_nil`, `head?_coeffList`, `coeffList_zero`, `coeffList_neg`, `coeffList_monomial`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeffList_C` 📖	mathematical	—	`coeffList` `DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`degree_eq_natDegree` `C_ne_zero` `natDegree_C` `CharP.cast_eq_zero` `CharP.ofCharZero` `WithBot.charZero` `Nat.instCharZero` `coeff_C_zero`
`coeffList_C_mul` 📖	mathematical	—	`coeffList` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`MulZeroClass.mul_zero` `coeffList_zero` `degree_mul` `degree_C` `zero_add` `coeff_C_mul`
`coeffList_eq_cons_leadingCoeff` 📖	mathematical	—	`coeffList` `leadingCoeff`	—	`withBotSucc_degree_eq_natDegree_add_one`
`coeffList_eq_nil` 📖	mathematical	—	`coeffList` `Polynomial` `instZero`	—	`Nat.instCanonicallyOrderedAdd` `Nat.instNoMaxOrder`
`coeffList_eraseLead` 📖	mathematical	—	`coeffList` `leadingCoeff` `natDegree` `WithBot.succ` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instSuccOrder` `degree` `eraseLead` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`eq_C_of_natDegree_eq_zero` `coeffList_C` `C_ne_zero` `leadingCoeff_C` `natDegree_C` `eraseLead_C` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `coeffList_zero` `zero_add` `eraseLead_add_monomial_natDegree_leadingCoeff` `coeffList_monomial` `leadingCoeff_ne_zero` `tsub_zero` `withBotSucc_degree_eq_natDegree_add_one` `eraseLead_natDegree_le` `coeffList_eq_cons_leadingCoeff` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instNoMaxOrder` `ExistsAddOfLE.exists_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `eraseLead_coeff_of_ne` `coeff_eq_zero_of_natDegree_lt`
`coeffList_monomial` 📖	mathematical	—	`coeffList` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`monomial_eq_zero_iff` `length_coeffList_eq_ite` `natDegree_monomial` `leadingCoeff_monomial` `coeffList_eq_cons_leadingCoeff` `natDegree_monomial_eq` `withBotSucc_degree_eq_natDegree_add_one` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `coeff_monomial_of_ne`
`coeffList_neg` 📖	mathematical	—	`coeffList` `Ring.toSemiring` `Polynomial` `instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`coeffList_zero` `neg_zero` `degree_neg` `coeff_neg`
`coeffList_zero` 📖	mathematical	—	`coeffList` `Polynomial` `instZero`	—	—
`head?_coeffList` 📖	mathematical	—	`coeffList` `leadingCoeff`	—	`coeffList_eq_cons_leadingCoeff`
`head_coeffList` 📖	mathematical	—	`coeffList` `leadingCoeff`	—	`Iff.not` `coeffList_eq_nil` `coeffList_eq_cons_leadingCoeff` `head?_coeffList`
`leadingCoeff_cons_eraseLead` 📖	mathematical	—	`leadingCoeff` `coeffList` `eraseLead`	—	`ne_zero_of_natDegree_gt` `natDegree_pos_of_nextCoeff_ne_zero` `nextCoeff_eq_zero_of_eraseLead_eq_zero` `withBotSucc_degree_eq_natDegree_add_one` `natDegree_eraseLead_add_one` `eraseLead_coeff_of_ne` `LT.lt.ne`
`length_coeffList_eq_ite` 📖	mathematical	—	`coeffList` `Polynomial` `instZero` `instDecidableEq` `natDegree`	—	`withBotSucc_degree_eq_natDegree_add_one`
`length_coeffList_eq_withBotSucc_degree` 📖	mathematical	—	`coeffList` `WithBot.succ` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instSuccOrder` `degree`	—	—

---

← Back to Index