Documentation Verification Report

Derivative

📁 Source: Mathlib/RingTheory/PowerSeries/Derivative.lean

Statistics

Metric	Count
Definitions `derivative`, `derivativeFun`, `«termD⁄dX»`	3
Theorems `coeff_derivative`, `coeff_derivativeFun`, `ext`, `derivativeFun_C`, `derivativeFun_add`, `derivativeFun_coe`, `derivativeFun_mul`, `derivativeFun_one`, `derivativeFun_smul`, `derivative_C`, `derivative_X`, `derivative_coe`, `derivative_inv`, `derivative_inv'`, `derivative_invOf`, `derivative_pow`, `derivative_subst`, `trunc_derivative`, `trunc_derivative'`, `trunc_derivativeFun`	20
Total	23

PowerSeries

Definitions

Name	Category	Theorems
`derivative` 📖	CompOp	12 math math: `derivative_exp`, `derivative_inv'`, `derivative_invOf`, `derivative_coe`, `coeff_derivative`, `derivative_subst`, `derivative_C`, `trunc_derivative`, `derivative_inv`, `derivative_X`, `derivative_pow`, `trunc_derivative'`
`derivativeFun` 📖	CompOp	8 math math: `derivativeFun_smul`, `coeff_derivativeFun`, `derivativeFun_C`, `derivativeFun_coe`, `derivativeFun_one`, `derivativeFun_add`, `trunc_derivativeFun`, `derivativeFun_mul`
`«termD⁄dX»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_derivative` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `MvPowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPowerSeries.instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `Derivation` `MvPowerSeries.instCommSemiring` `MvPowerSeries.instAlgebra` `Algebra.id` `Derivation.instFunLike` `derivative` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toAdd` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoidWithOne.toOne`	—	`coeff_derivativeFun`
`coeff_derivativeFun` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `MvPowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `MvPowerSeries.instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `derivativeFun` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toAdd` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoidWithOne.toOne`	—	`derivativeFun.eq_1`
`derivativeFun_C` 📖	mathematical	—	`derivativeFun` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPowerSeries.instSemiring` `RingHom.instFunLike` `C` `MvPowerSeries.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`ext` `coeff_derivativeFun` `coeff_succ_C` `MulZeroClass.zero_mul` `LinearMap.map_zero`
`derivativeFun_add` 📖	mathematical	—	`derivativeFun` `PowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPowerSeries.instSemiring` `CommSemiring.toSemiring`	—	`ext` `coeff_derivativeFun` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `add_mul` `Distrib.rightDistribClass`
`derivativeFun_coe` 📖	mathematical	—	`derivativeFun` `Polynomial.toPowerSeries` `CommSemiring.toSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.derivative`	—	`ext` `coeff_derivativeFun` `Polynomial.coeff_coe` `Polynomial.coeff_derivative`
`derivativeFun_mul` 📖	mathematical	—	`derivativeFun` `PowerSeries` `MvPowerSeries.instMul` `CommSemiring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MvPowerSeries.instSemiring` `Algebra.toSMul` `MvPowerSeries.instCommSemiring` `Algebra.id`	—	`ext` `coeff_derivativeFun` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `coeff_mul_eq_coeff_trunc_mul_trunc` `smul_eq_mul` `coeff_mul_eq_coeff_trunc_mul_trunc₂` `trunc_derivativeFun`
`derivativeFun_one` 📖	mathematical	—	`derivativeFun` `PowerSeries` `MvPowerSeries.instOne` `CommSemiring.toSemiring` `MvPowerSeries.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `derivativeFun_C`
`derivativeFun_smul` 📖	mathematical	—	`derivativeFun` `PowerSeries` `Algebra.toSMul` `MvPowerSeries.instSemiring` `CommSemiring.toSemiring` `MvPowerSeries.instAlgebra` `Algebra.id`	—	`smul_eq_C_mul` `derivativeFun_mul` `derivativeFun_C` `smul_zero` `add_zero` `smul_eq_mul`
`derivative_C` 📖	mathematical	—	`DFunLike.coe` `Derivation` `PowerSeries` `MvPowerSeries.instCommSemiring` `MvPowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPowerSeries.instAlgebra` `Algebra.id` `Semiring.toModule` `MvPowerSeries.instModule` `Derivation.instFunLike` `derivative` `RingHom` `MvPowerSeries.instSemiring` `RingHom.instFunLike` `C` `MvPowerSeries.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`derivativeFun_C`
`derivative_X` 📖	mathematical	—	`DFunLike.coe` `Derivation` `PowerSeries` `MvPowerSeries.instCommSemiring` `MvPowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPowerSeries.instAlgebra` `Algebra.id` `Semiring.toModule` `MvPowerSeries.instModule` `Derivation.instFunLike` `derivative` `X` `MvPowerSeries.instOne`	—	`ext` `coeff_derivative` `coeff_X` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `boole_mul` `coeff_one` `Nat.cast_zero` `zero_add`
`derivative_coe` 📖	mathematical	—	`DFunLike.coe` `Derivation` `PowerSeries` `MvPowerSeries.instCommSemiring` `MvPowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPowerSeries.instAlgebra` `Algebra.id` `Semiring.toModule` `MvPowerSeries.instModule` `Derivation.instFunLike` `derivative` `Polynomial.toPowerSeries` `LinearMap` `RingHom.id` `Polynomial` `Polynomial.semiring` `Polynomial.module` `LinearMap.instFunLike` `Polynomial.derivative`	—	`derivativeFun_coe`
`derivative_inv` 📖	mathematical	—	`DFunLike.coe` `Derivation` `PowerSeries` `CommRing.toCommSemiring` `MvPowerSeries.instCommSemiring` `MvPowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPowerSeries.instAlgebra` `Algebra.id` `Semiring.toModule` `MvPowerSeries.instModule` `Derivation.instFunLike` `derivative` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MvPowerSeries.instSemiring` `Units` `Units.instInv` `MvPowerSeries.instMul` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `MvPowerSeries.instAddCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Monoid.toPow`	—	`Derivation.leibniz_of_mul_eq_one` `Units.inv_mul`
`derivative_inv'` 📖	mathematical	—	`DFunLike.coe` `Derivation` `PowerSeries` `Semifield.toCommSemiring` `Field.toSemifield` `MvPowerSeries.instCommSemiring` `MvPowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPowerSeries.instAlgebra` `Algebra.id` `Semiring.toModule` `MvPowerSeries.instModule` `Derivation.instFunLike` `derivative` `MvPowerSeries.instInv` `MvPowerSeries.instMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `MvPowerSeries.instAddCommGroup` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MvPowerSeries.instSemiring`	—	`MvPowerSeries.inv_eq_zero` `pow_two` `MulZeroClass.zero_mul` `neg_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `Derivation.instAddMonoidHomClass` `Derivation.leibniz_of_mul_eq_one` `inv_mul_cancel`
`derivative_invOf` 📖	mathematical	—	`DFunLike.coe` `Derivation` `PowerSeries` `CommRing.toCommSemiring` `MvPowerSeries.instCommSemiring` `MvPowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPowerSeries.instAlgebra` `Algebra.id` `Semiring.toModule` `MvPowerSeries.instModule` `Derivation.instFunLike` `derivative` `Invertible.invOf` `MvPowerSeries.instMul` `MvPowerSeries.instOne` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `MvPowerSeries.instAddCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MvPowerSeries.instSemiring`	—	`Derivation.leibniz_invOf` `smul_eq_mul`
`derivative_pow` 📖	mathematical	—	`DFunLike.coe` `Derivation` `PowerSeries` `MvPowerSeries.instCommSemiring` `MvPowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPowerSeries.instAlgebra` `Algebra.id` `Semiring.toModule` `MvPowerSeries.instModule` `Derivation.instFunLike` `derivative` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MvPowerSeries.instSemiring` `MvPowerSeries.instMul` `AddMonoidWithOne.toNatCast` `MvPowerSeries.instAddMonoidWithOne`	—	`Derivation.leibniz_pow` `smul_eq_mul` `nsmul_eq_mul` `mul_assoc`
`derivative_subst` 📖	mathematical	`HasSubst`	`DFunLike.coe` `Derivation` `PowerSeries` `CommRing.toCommSemiring` `MvPowerSeries.instCommSemiring` `MvPowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPowerSeries.instAlgebra` `Algebra.id` `Semiring.toModule` `MvPowerSeries.instModule` `Derivation.instFunLike` `derivative` `subst` `MvPowerSeries` `MvPowerSeries.instMul`	—	`ext` `Filter.Eventually.exists_forall_of_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `HasSubst.eventually_coeff_pow_eq_zero` `coeff_subst'` `finsum_congr` `lt_or_ge` `coeff_coe_trunc_of_lt` `instReflLe` `MulZeroClass.mul_zero` `Polynomial.coeff_coe` `coeff_trunc` `Nat.instNoMaxOrder` `coeff_derivative` `coeff_mul` `Finset.sum_congr` `MulZeroClass.zero_mul`
`trunc_derivative` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `Polynomial` `MvPowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `MvPowerSeries.instModule` `Semiring.toModule` `Polynomial.module` `LinearMap.instFunLike` `trunc` `Derivation` `MvPowerSeries.instCommSemiring` `MvPowerSeries.instAlgebra` `Algebra.id` `Derivation.instFunLike` `derivative` `Polynomial.derivative`	—	`trunc_derivativeFun`
`trunc_derivative'` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `Polynomial` `MvPowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `MvPowerSeries.instModule` `Semiring.toModule` `Polynomial.module` `LinearMap.instFunLike` `trunc` `Derivation` `MvPowerSeries.instCommSemiring` `MvPowerSeries.instAlgebra` `Algebra.id` `Derivation.instFunLike` `derivative` `Polynomial.derivative`	—	`zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `trunc_derivative` `zero_add` `trunc_one_left` `coeff_zero_eq_constantCoeff` `Polynomial.derivative_C` `Polynomial.derivative_zero` `add_tsub_cancel_right` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`trunc_derivativeFun` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `Polynomial` `MvPowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `MvPowerSeries.instModule` `Semiring.toModule` `Polynomial.module` `LinearMap.instFunLike` `trunc` `derivativeFun` `Polynomial.derivative`	—	`Polynomial.ext` `coeff_trunc` `coeff_derivativeFun` `Polynomial.coeff_derivative` `MulZeroClass.zero_mul`

PowerSeries.derivative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`DFunLike.coe` `Derivation` `PowerSeries` `CommRing.toCommSemiring` `MvPowerSeries.instCommSemiring` `MvPowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPowerSeries.instAlgebra` `Algebra.id` `Semiring.toModule` `MvPowerSeries.instModule` `Derivation.instFunLike` `PowerSeries.derivative` `RingHom` `MvPowerSeries.instSemiring` `RingHom.instFunLike` `PowerSeries.constantCoeff`	—	—	`PowerSeries.ext` `PowerSeries.coeff_zero_eq_constantCoeff` `IsAddTorsionFree.to_isTorsionFree_nat` `Nat.instIsCancelMulZero` `nsmul_eq_mul` `mul_comm` `Nat.cast_succ` `PowerSeries.coeff_derivative`

---

← Back to Index