Documentation Verification Report

SumIteratedDerivative

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

Statistics

Metric	Count
Definitions `sumIDeriv`	1
Theorems `aeval_iterate_derivative_of_ge`, `aeval_iterate_derivative_of_lt`, `aeval_iterate_derivative_self`, `aeval_sumIDeriv`, `aeval_sumIDeriv_eq_eval`, `aeval_sumIDeriv_of_pos`, `eval_sumIDeriv_of_pos`, `exists_iterate_derivative_eq_factorial_smul`, `sumIDeriv_C`, `sumIDeriv_X`, `sumIDeriv_apply`, `sumIDeriv_apply_of_le`, `sumIDeriv_apply_of_lt`, `sumIDeriv_derivative`, `sumIDeriv_eq_self_add`, `sumIDeriv_map`	16
Total	17

Polynomial

Definitions

Name	Category	Theorems
`sumIDeriv` 📖	CompOp	14 math math: `sumIDeriv_map`, `aeval_sumIDeriv`, `sumIDeriv_C`, `sumIDeriv_eq_self_add`, `sumIDeriv_apply`, `sumIDeriv_X`, `LindemannWeierstrass.integral_exp_mul_eval`, `eval_sumIDeriv_of_pos`, `sumIDeriv_derivative`, `aeval_sumIDeriv_eq_eval`, `sumIDeriv_apply_of_le`, `sumIDeriv_apply_of_lt`, `LindemannWeierstrass.hasDerivAt_cexp_mul_sumIDeriv`, `aeval_sumIDeriv_of_pos`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_iterate_derivative_of_ge` 📖	mathematical	—	`natDegree` `CommSemiring.toSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `CommRing.toCommSemiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `Nat.iterate` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `derivative` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.factorial`	—	`exists_iterate_derivative_eq_factorial_smul` `LE.le.trans` `natDegree_C_mul_le` `nsmul_eq_mul` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_natCast` `AlgHomClass.toRingHomClass` `Nat.add_descFactorial_eq_ascFactorial` `Nat.factorial_mul_ascFactorial`
`aeval_iterate_derivative_of_lt` 📖	mathematical	`map` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap` `Polynomial` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `instSub` `CommRing.toRing` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	`AlgHom` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `Nat.iterate` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `derivative` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`pow_add` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `LE.le.trans` `le_tsub_of_add_le_left` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `tsub_le_tsub_left` `tsub_le_self` `aeval_def` `eval₂_eq_eval_map` `iterate_derivative_map` `iterate_derivative_mul` `Finset.sum_congr` `iterate_derivative_X_sub_pow` `IsScalarTower.right` `smul_smul` `Algebra.to_smulCommClass` `mul_assoc` `eval_mul` `pow_one` `eval_sub` `eval_X` `eval_C` `sub_self` `MulZeroClass.zero_mul`
`aeval_iterate_derivative_self` 📖	mathematical	`map` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebraMap` `Polynomial` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `instSub` `CommRing.toRing` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	`AlgHom` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `Nat.iterate` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `derivative` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.factorial` `eval`	—	`pow_add` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `tsub_tsub_cancel_of_le` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `aeval_def` `eval₂_eq_eval_map` `iterate_derivative_map` `iterate_derivative_mul` `Finset.sum_congr` `iterate_derivative_X_sub_pow` `IsScalarTower.right` `smul_smul` `Finset.sum_range_succ'` `Nat.choose_zero_right` `one_mul` `tsub_zero` `Nat.descFactorial_self` `tsub_self` `pow_zero` `smul_mul_assoc` `Function.iterate_zero_apply` `eval_add` `eval_smul` `eval_finset_sum` `Finset.sum_eq_zero` `le_add_self` `Finset.mem_range` `pow_one` `eval_mul` `eval_sub` `eval_X` `eval_C` `sub_self` `MulZeroClass.zero_mul` `smul_zero` `zero_add`
`aeval_sumIDeriv` 📖	mathematical	—	`natDegree` `CommSemiring.toSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `CommRing.toCommSemiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `sumIDeriv` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.factorial`	—	`lt_or_ge` `natDegree_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `smul_zero` `aeval_iterate_derivative_of_lt` `aeval_iterate_derivative_of_ge` `LE.le.trans` `tsub_le_tsub_left` `Nat.instOrderedSub` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `natDegree_sum_le` `instCommutativeMax` `instAssociativeMax` `Finset.fold_max_le` `sumIDeriv_apply` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `Finset.sum_congr` `Finset.smul_sum`
`aeval_sumIDeriv_eq_eval` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `CommRing.toCommSemiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `sumIDeriv` `eval` `map` `algebraMap`	—	`aeval_def` `eval.eq_1` `sumIDeriv_map` `eval₂_map` `RingHom.id_comp`
`aeval_sumIDeriv_of_pos` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	`natDegree` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `sumIDeriv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.factorial` `eval`	—	`eq_or_ne` `natDegree_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `smul_zero` `add_zero` `mul_eq_zero` `instNoZeroDivisors` `map_zero` `X_sub_C_ne_zero` `eq_zero_of_pow_eq_zero` `isReduced_of_noZeroDivisors` `eval_zero` `aeval_iterate_derivative_of_ge` `LE.le.trans` `natDegree_sum_le` `instCommutativeMax` `instAssociativeMax` `Finset.fold_max_le` `tsub_le_tsub_left` `Nat.instOrderedSub` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finset.mem_Ico` `Finset.range_eq_Ico` `Finset.Ico_union_Ico_eq_Ico` `LT.lt.le` `tsub_le_iff_right` `le_self_add` `Nat.instCanonicallyOrderedAdd` `natDegree_mul` `pow_ne_zero` `map_eq_zero_iff` `MulZeroClass.mul_zero` `natDegree_pow` `natDegree_X_sub_C` `mul_one` `natDegree_map_le` `zero_add` `sumIDeriv_apply` `map_sum` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Finset.sum_union` `Finset.disjoint_iff_inter_eq_empty` `Finset.eq_empty_iff_forall_notMem` `LT.lt.not_ge` `Finset.mem_inter` `Finset.sum_range_succ` `Finset.sum_eq_zero` `aeval_iterate_derivative_of_lt` `Finset.mem_range` `aeval_iterate_derivative_self` `Finset.smul_sum` `Finset.sum_congr`
`eval_sumIDeriv_of_pos` 📖	mathematical	—	`natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `eval` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `sumIDeriv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.factorial`	—	`nsmul_eq_mul` `map_id` `aeval_sumIDeriv_of_pos`
`exists_iterate_derivative_eq_factorial_smul` 📖	mathematical	—	`natDegree` `Nat.iterate` `Polynomial` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `derivative` `instNSMul` `Nat.factorial`	—	`LE.le.trans` `natDegree_sum_le` `instCommutativeMax` `instAssociativeMax` `Finset.fold_max_le` `natDegree_C_mul_le` `natDegree_X_pow_le` `le_natDegree_of_mem_supp` `natDegree_iterate_derivative` `iterate_derivative_eq_factorial_smul_sum`
`sumIDeriv_C` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `sumIDeriv` `RingHom` `RingHom.instFunLike` `C`	—	`sumIDeriv_apply` `natDegree_C` `zero_add` `Finset.sum_range_one` `Function.iterate_zero_apply`
`sumIDeriv_X` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Nat.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `sumIDeriv` `X` `instAdd` `RingHom` `RingHom.instFunLike` `C`	—	`sumIDeriv_apply` `natDegree_X` `Nat.instNontrivial` `Finset.sum_range_succ` `Finset.sum_range_one` `Function.iterate_zero_apply` `Function.iterate_one` `derivative_X` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one`
`sumIDeriv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `sumIDeriv` `Finset.sum` `Finset.range` `natDegree` `Nat.iterate` `derivative`	—	`Finsupp.sum_of_support_subset` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instZeroLEOneClass` `Nat.instNoMaxOrder`
`sumIDeriv_apply_of_le` 📖	mathematical	`natDegree`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `sumIDeriv` `Finset.sum` `Finset.range` `Nat.iterate` `derivative`	—	`Finsupp.sum_of_support_subset` `Nat.instNoMaxOrder`
`sumIDeriv_apply_of_lt` 📖	mathematical	`natDegree`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `sumIDeriv` `Finset.sum` `Finset.range` `Nat.iterate` `derivative`	—	`Finsupp.sum_of_support_subset`
`sumIDeriv_derivative` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `sumIDeriv` `derivative`	—	`sumIDeriv_apply_of_le` `LE.le.trans` `natDegree_derivative_le` `tsub_le_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `sumIDeriv_apply` `derivative_sum` `Finset.sum_congr` `Function.iterate_succ_apply'`
`sumIDeriv_eq_self_add` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `sumIDeriv` `instAdd` `derivative`	—	`sumIDeriv_apply` `derivative_sum` `Finset.sum_range_succ'` `Finset.sum_range_succ` `add_comm` `add_zero` `Finset.sum_congr` `Function.iterate_succ_apply'` `iterate_derivative_eq_zero`
`sumIDeriv_map` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `sumIDeriv` `map`	—	`sumIDeriv_apply_of_le` `le_max_left` `le_max_right` `map_sum` `Finset.sum_congr` `iterate_derivative_map`

---

← Back to Index