Documentation Verification Report

Inductions

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

Statistics

Metric	Count
Definitions `divX`, `divX_hom`, `recOnHorner`	3
Theorems `X_mul_divX_add`, `coeff_divX`, `degree_divX_lt`, `degree_pos_induction_on`, `divX_C`, `divX_C_mul`, `divX_C_mul_X_pow`, `divX_X_pow`, `divX_add`, `divX_eq_zero_iff`, `divX_hom_toFun`, `divX_mul_X_add`, `divX_one`, `divX_zero`, `natDegree_divX_eq_natDegree_tsub_one`, `natDegree_divX_le`, `natDegree_ne_zero_induction_on`	17
Total	20

Polynomial

Definitions

Name	Category	Theorems
`divX` 📖	CompOp	19 math math: `divX_X_pow`, `Matrix.det_one_add_smul`, `degree_divX_lt`, `divX_eq_zero_iff`, `divX_hom_toFun`, `X_mul_divX_add`, `natDegree_divX_le`, `divX_add`, `divX_mul_X_add`, `Matrix.det_one_add_X_smul`, `divX_C_mul`, `divX_zero`, `divX_C_mul_X_pow`, `divX_C`, `coeff_divX`, `divX_one`, `natDegree_divX_eq_natDegree_tsub_one`, `inv_eq_of_aeval_divX_ne_zero`, `inv_eq_of_root_of_coeff_zero_ne_zero`
`divX_hom` 📖	CompOp	1 math math: `divX_hom_toFun`
`recOnHorner` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`X_mul_divX_add` 📖	mathematical	—	`Polynomial` `instAdd` `instMul` `X` `divX` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `coeff`	—	`ext` `coeff_add` `mul_coeff_zero` `coeff_X_zero` `coeff_divX` `zero_add` `MulZeroClass.zero_mul` `coeff_C` `coeff_X_mul` `coeff_C_succ` `add_zero`
`coeff_divX` 📖	mathematical	—	`coeff` `divX`	—	`add_comm`
`degree_divX_lt` 📖	mathematical	—	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `divX`	—	`eq_C_of_degree_le_zero` `divX_C` `degree_zero` `MulZeroClass.zero_mul` `zero_add` `lt_of_le_of_ne` `bot_le` `degree_eq_bot` `coeff_C_zero` `Monic.leadingCoeff` `mul_one` `degree_C_le` `degree_X` `Nontrivial.of_polynomial_ne` `degree_mul'` `add_le_add` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.addRightMono` `covariant_swap_add_of_covariant_add` `zero_le_degree_iff` `divX_eq_zero_iff` `le_rfl` `degree_add_eq_left_of_degree_lt` `degree_lt_degree_mul_X` `divX_mul_X_add`
`degree_pos_induction_on` 📖	—	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `degree` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `X` `instAdd`	—	—	`degree_zero` `lt_of_not_ge` `not_lt_of_ge` `degree_C_le` `zero_add` `C_add` `eq_C_of_degree_le_zero` `le_of_not_gt` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `MulZeroClass.zero_mul`
`divX_C` 📖	mathematical	—	`divX` `DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `instZero`	—	`ext` `coeff_divX` `coeff_C_succ`
`divX_C_mul` 📖	mathematical	—	`divX` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`ext` `coeff_divX` `coeff_C_mul`
`divX_C_mul_X_pow` 📖	mathematical	—	`divX` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `instZero`	—	`divX_C_mul` `divX_X_pow` `mul_ite` `MulZeroClass.mul_zero`
`divX_X_pow` 📖	mathematical	—	`divX` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instZero`	—	`pow_zero` `divX_one` `ext` `coeff_divX` `coeff_X_pow` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`divX_add` 📖	mathematical	—	`divX` `Polynomial` `instAdd`	—	`ext` `coeff_divX` `coeff_add`
`divX_eq_zero_iff` 📖	mathematical	—	`divX` `Polynomial` `instZero` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `coeff`	—	`MulZeroClass.zero_mul` `zero_add` `divX_mul_X_add` `divX_C`
`divX_hom_toFun` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Polynomial` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `semiring` `AddMonoidHom.instFunLike` `divX_hom` `divX`	—	—
`divX_mul_X_add` 📖	mathematical	—	`Polynomial` `instAdd` `instMul` `divX` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `coeff`	—	`ext` `coeff_add` `mul_coeff_zero` `coeff_divX` `zero_add` `coeff_X_zero` `MulZeroClass.mul_zero` `coeff_C` `coeff_mul_X` `coeff_C_succ` `add_zero`
`divX_one` 📖	mathematical	—	`divX` `Polynomial` `instOne` `instZero`	—	`ext` `coeff_divX` `coeff_one`
`divX_zero` 📖	mathematical	—	`divX` `Polynomial` `instZero`	—	`leadingCoeff_eq_zero`
`natDegree_divX_eq_natDegree_tsub_one` 📖	mathematical	—	`natDegree` `divX`	—	`map_natDegree_eq_sub` `AddMonoidHom.instAddMonoidHomClass` `eq_C_of_natDegree_eq_zero` `C_mul_X_pow_eq_monomial` `divX_hom_toFun` `divX_C_mul` `divX_X_pow` `MulZeroClass.mul_zero` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `natDegree_C_mul_X_pow`
`natDegree_divX_le` 📖	mathematical	—	`natDegree` `divX`	—	`Eq.trans_le` `natDegree_divX_eq_natDegree_tsub_one`
`natDegree_ne_zero_induction_on` 📖	—	`Polynomial` `instAdd` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial`	—	—	`induction_on` `natDegree_C` `eq_C_of_natDegree_eq_zero` `C_add` `add_comm` `C_0` `MulZeroClass.zero_mul` `natDegree_zero` `C_mul_X_pow_eq_monomial`

---

← Back to Index