Pow

📁 Source: Mathlib/Analysis/Calculus/FDeriv/Pow.lean

Statistics

Metric	Count
Definitions	0
Theorems fun_pow, pow, fun_pow, pow, fun_pow, pow, fun_pow, pow, fun_pow', pow, pow', fun_pow', pow, pow', fun_pow', pow, pow', differentiableAt_pow, differentiableOn_pow, differentiableWithinAt_pow, differentiable_pow, fderivWithin_fun_pow, fderivWithin_fun_pow', fderivWithin_pow, fderivWithin_pow', fderivWithin_pow_ring, fderivWithin_pow_ring', fderiv_fun_pow, fderiv_fun_pow', fderiv_pow, fderiv_pow', fderiv_pow_ring, fderiv_pow_ring', hasFDerivAt_pow, hasFDerivAt_pow', hasFDerivWithinAt_pow, hasFDerivWithinAt_pow', hasStrictFDerivAt_pow, hasStrictFDerivAt_pow'	39
Total	39

Differentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fun_pow 📖	mathematical	Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing	—	DifferentiableAt.pow
pow 📖	mathematical	Differentiable NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing	—	fun_pow

DifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fun_pow 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing	—	differentiableWithinAt_univ DifferentiableWithinAt.pow differentiableWithinAt
pow 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing	—	fun_pow

DifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fun_pow 📖	mathematical	DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing	—	DifferentiableWithinAt.pow
pow 📖	mathematical	DifferentiableOn NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing	—	fun_pow

DifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fun_pow 📖	mathematical	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul HasFDerivWithinAt.pow'
pow 📖	mathematical	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing	—	fun_pow

HasFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fun_pow' 📖	mathematical	HasFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Finset.sum ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MulOpposite.instSemiring Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul pow_zero Finset.sum_congr zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub one_smul hasFDerivAt_const pow_one tsub_self Finset.sum_singleton mul' pow_succ' congr_fderiv
pow 📖	mathematical	HasFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedAlgebra.toNormedSpace SeminormedCommRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid	—	congr_fderiv IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul pow'
pow' 📖	mathematical	HasFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Finset.sum ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MulOpposite.instSemiring Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul	—	fun_pow'

HasFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fun_pow' 📖	mathematical	HasFDerivWithinAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Finset.sum ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MulOpposite.instSemiring Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul pow_zero Finset.sum_congr zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub one_smul hasFDerivWithinAt_const pow_one tsub_self Finset.sum_singleton mul' pow_succ' congr_fderiv
pow 📖	mathematical	HasFDerivWithinAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedAlgebra.toNormedSpace SeminormedCommRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid	—	congr_fderiv IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul pow'
pow' 📖	mathematical	HasFDerivWithinAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Finset.sum ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MulOpposite.instSemiring Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul	—	fun_pow'

HasStrictFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fun_pow' 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Finset.sum ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MulOpposite.instSemiring Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul pow_zero Finset.sum_congr zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub one_smul hasStrictFDerivAt_const pow_one tsub_self Finset.sum_singleton mul' pow_succ' congr_fderiv
pow 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedAlgebra.toNormedSpace SeminormedCommRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid	—	congr_fderiv IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul pow'
pow' 📖	mathematical	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Finset.sum ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MulOpposite.instSemiring Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul	—	fun_pow'

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiableAt_pow 📖	mathematical	—	DifferentiableAt NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedSpace.toModule NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing	—	DifferentiableAt.pow differentiableAt_id
differentiableOn_pow 📖	mathematical	—	DifferentiableOn NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedSpace.toModule NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing	—	DifferentiableOn.pow differentiableOn_id
differentiableWithinAt_pow 📖	mathematical	—	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedSpace.toModule NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing	—	DifferentiableWithinAt.pow differentiableWithinAt_id
differentiable_pow 📖	mathematical	—	Differentiable NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedSpace.toModule NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing	—	Differentiable.pow differentiable_id
fderivWithin_fun_pow 📖	mathematical	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DifferentiableWithinAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedAlgebra.toNormedSpace SeminormedCommRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	fderivWithin Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	HasFDerivWithinAt.fderivWithin Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsTopologicalSemiring.toContinuousAdd TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace HasFDerivWithinAt.pow DifferentiableWithinAt.hasFDerivWithinAt
fderivWithin_fun_pow' 📖	mathematical	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DifferentiableWithinAt NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	fderivWithin Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Finset.sum ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MulOpposite.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul	—	HasFDerivWithinAt.fderivWithin IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace HasFDerivWithinAt.pow' DifferentiableWithinAt.hasFDerivWithinAt
fderivWithin_pow 📖	mathematical	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DifferentiableWithinAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedAlgebra.toNormedSpace SeminormedCommRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	fderivWithin Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	fderivWithin_fun_pow
fderivWithin_pow' 📖	mathematical	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DifferentiableWithinAt NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	fderivWithin Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Finset.sum ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MulOpposite.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul	—	fderivWithin_fun_pow'
fderivWithin_pow_ring 📖	mathematical	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedAlgebra.toNormedSpace SeminormedCommRing.toSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace	fderivWithin Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.id	—	Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing fderivWithin_fun_pow DifferentiableAt.differentiableWithinAt differentiableAt_fun_id fderivWithin_id' IsTopologicalSemiring.toContinuousAdd IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
fderivWithin_pow_ring' 📖	mathematical	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace	fderivWithin Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Finset.sum ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MulOpposite.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul ContinuousLinearMap.id	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul fderivWithin_fun_pow' DifferentiableAt.differentiableWithinAt differentiableAt_fun_id fderivWithin_id' IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
fderiv_fun_pow 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedAlgebra.toNormedSpace SeminormedCommRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	fderiv Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	HasFDerivAt.fderiv Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsTopologicalSemiring.toContinuousAdd TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace HasFDerivAt.pow DifferentiableAt.hasFDerivAt
fderiv_fun_pow' 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	fderiv Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Finset.sum ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MulOpposite.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul	—	HasFDerivAt.fderiv IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace HasFDerivAt.pow' DifferentiableAt.hasFDerivAt
fderiv_pow 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedAlgebra.toNormedSpace SeminormedCommRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	fderiv Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	fderiv_fun_pow
fderiv_pow' 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing SeminormedRing.toPseudoMetricSpace	fderiv Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Finset.sum ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MulOpposite.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul	—	fderiv_fun_pow'
fderiv_pow_ring 📖	mathematical	—	fderiv NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedAlgebra.toNormedSpace SeminormedCommRing.toSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.id	—	Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing fderiv_fun_pow differentiableAt_fun_id fderiv_id' IsTopologicalSemiring.toContinuousAdd IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
fderiv_pow_ring' 📖	mathematical	—	fderiv NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedSpace.toModule NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Finset.sum ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MulOpposite.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul ContinuousLinearMap.id	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul fderiv_fun_pow' differentiableAt_fun_id fderiv_id' IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
hasFDerivAt_pow 📖	mathematical	—	HasFDerivAt SeminormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAlgebra.toNormedSpace SeminormedCommRing.toSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ContinuousLinearMap.id	—	HasFDerivAt.pow hasFDerivAt_id
hasFDerivAt_pow' 📖	mathematical	—	HasFDerivAt NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedSpace.toModule NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Finset.sum ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MulOpposite.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul ContinuousLinearMap.id	—	HasFDerivAt.pow' hasFDerivAt_id
hasFDerivWithinAt_pow 📖	mathematical	—	HasFDerivWithinAt SeminormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAlgebra.toNormedSpace SeminormedCommRing.toSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ContinuousLinearMap.id	—	HasFDerivWithinAt.pow hasFDerivWithinAt_id
hasFDerivWithinAt_pow' 📖	mathematical	—	HasFDerivWithinAt NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedSpace.toModule NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Finset.sum ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MulOpposite.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul ContinuousLinearMap.id	—	HasFDerivWithinAt.pow' hasFDerivWithinAt_id
hasStrictFDerivAt_pow 📖	mathematical	—	HasStrictFDerivAt SeminormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAlgebra.toNormedSpace SeminormedCommRing.toSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ContinuousLinearMap.id	—	HasStrictFDerivAt.pow hasStrictFDerivAt_id
hasStrictFDerivAt_pow' 📖	mathematical	—	HasStrictFDerivAt NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedSpace.toModule NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedAlgebra.toNormedSpace NormedRing.toSeminormedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Finset.sum ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction MulOpposite.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul_op SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Ring.uniformContinuousConstSMul ContinuousLinearMap.id	—	HasStrictFDerivAt.pow' hasStrictFDerivAt_id

---

← Back to Index