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 instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModule Semiring.toModule LinearMap.instFunLike coeff Derivation instCommSemiring 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 instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring 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 instSemiring RingHom.instFunLike C 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 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 instSemiring Algebra.toSMul 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 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 instSemiring CommSemiring.toSemiring 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 instCommSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instAlgebra Algebra.id Semiring.toModule instModule Derivation.instFunLike derivative RingHom instSemiring RingHom.instFunLike C instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	derivativeFun_C
derivative_X 📖	mathematical	—	DFunLike.coe Derivation PowerSeries instCommSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instAlgebra Algebra.id Semiring.toModule instModule Derivation.instFunLike derivative X MvPowerSeries.instOne	—	ext coeff_derivative coeff_X AddRightCancelSemigroup.toIsRightCancelAdd boole_mul coeff_one Nat.cast_zero zero_add
derivative_coe 📖	mathematical	—	DFunLike.coe Derivation PowerSeries instCommSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instAlgebra Algebra.id Semiring.toModule 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 instCommSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instAlgebra Algebra.id Semiring.toModule instModule Derivation.instFunLike derivative Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring Units Units.instInv MvPowerSeries.instMul NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup Ring.toAddCommGroup CommRing.toRing Monoid.toNatPow	—	Derivation.leibniz_of_mul_eq_one Units.inv_mul
derivative_inv' 📖	mathematical	—	DFunLike.coe Derivation PowerSeries Semifield.toCommSemiring Field.toSemifield instCommSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instAlgebra Algebra.id Semiring.toModule instModule Derivation.instFunLike derivative instInv MvPowerSeries.instMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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 instCommSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instAlgebra Algebra.id Semiring.toModule instModule Derivation.instFunLike derivative Invertible.invOf MvPowerSeries.instMul MvPowerSeries.instOne NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup Ring.toAddCommGroup CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring	—	Derivation.leibniz_invOf smul_eq_mul
derivative_pow 📖	mathematical	—	DFunLike.coe Derivation PowerSeries CommRing.toCommSemiring instCommSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instAlgebra Algebra.id Semiring.toModule instModule Derivation.instFunLike derivative Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring MvPowerSeries.instMul AddMonoidWithOne.toNatCast MvPowerSeries.instAddMonoidWithOne	—	pow_zero Derivation.map_one_eq_zero Nat.cast_zero zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub mul_one MulZeroClass.zero_mul pow_succ Derivation.leibniz add_tsub_cancel_right IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid one_mul MulZeroClass.mul_zero add_zero zero_add Nat.cast_one Nat.cast_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_one
derivative_subst 📖	mathematical	HasSubst	DFunLike.coe Derivation PowerSeries CommRing.toCommSemiring instCommSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instAlgebra Algebra.id Semiring.toModule 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 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 instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc Derivation instCommSemiring instAlgebra Algebra.id Derivation.instFunLike derivative Polynomial.derivative	—	trunc_derivativeFun
trunc_derivative' 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring instModule Semiring.toModule Polynomial.module LinearMap.instFunLike trunc Derivation instCommSemiring 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 AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
trunc_derivativeFun 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries Polynomial instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring 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 PowerSeries.instCommSemiring PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring PowerSeries.instAlgebra Algebra.id Semiring.toModule PowerSeries.instModule Derivation.instFunLike PowerSeries.derivative RingHom PowerSeries.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