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	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.toPow 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	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.toPow 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	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.toPow 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	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.toPow 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	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.toPow 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	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.toPow 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	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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing	—	IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul 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	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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing	—	fun_pow

HasFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fun_pow' 📖	mathematical	HasFDerivAt 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	HasFDerivAt 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.toPow 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 IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid Module.toDistribMulAction MulOpposite.instSemiring Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul 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 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	HasFDerivAt 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 Monoid.toPow 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 ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNSMul ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid	—	congr_fderiv IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul pow'
pow' 📖	mathematical	HasFDerivAt 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	HasFDerivAt 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.toPow 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 IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid Module.toDistribMulAction MulOpposite.instSemiring Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	fun_pow'

HasFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fun_pow' 📖	mathematical	HasFDerivWithinAt 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	HasFDerivWithinAt 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.toPow 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 IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid Module.toDistribMulAction MulOpposite.instSemiring Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul 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 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	HasFDerivWithinAt 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 Monoid.toPow 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 ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNSMul ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid	—	congr_fderiv IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul pow'
pow' 📖	mathematical	HasFDerivWithinAt 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	HasFDerivWithinAt 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.toPow 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 IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid Module.toDistribMulAction MulOpposite.instSemiring Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	fun_pow'

HasStrictFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fun_pow' 📖	mathematical	HasStrictFDerivAt 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	HasStrictFDerivAt 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.toPow 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 IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid Module.toDistribMulAction MulOpposite.instSemiring Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul 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 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	HasStrictFDerivAt 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 Monoid.toPow 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 ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNSMul ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid	—	congr_fderiv IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul pow'
pow' 📖	mathematical	HasStrictFDerivAt 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	HasStrictFDerivAt 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.toPow 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 IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid Module.toDistribMulAction MulOpposite.instSemiring Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	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.toPow 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.toPow 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.toPow 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.toPow 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 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 Monoid.toPow 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 SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNSMul ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	HasFDerivWithinAt.fderivWithin Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsSemitopologicalSemiring.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 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.toPow 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 IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction MulOpposite.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	HasFDerivWithinAt.fderivWithin IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul 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 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 Pi.instPow Monoid.toPow 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 SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNSMul 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 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.toPow 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 IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction MulOpposite.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	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 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.toPow 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 SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNSMul ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.id	—	Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing fderivWithin_fun_pow DifferentiableAt.differentiableWithinAt differentiableAt_fun_id fderivWithin_id' IsSemitopologicalSemiring.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 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.toPow 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 IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction MulOpposite.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib ContinuousLinearMap.id	—	IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul 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 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 Monoid.toPow 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 SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNSMul ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	HasFDerivAt.fderiv Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsSemitopologicalSemiring.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 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.toPow 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 IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction MulOpposite.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	HasFDerivAt.fderiv IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul 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 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 Monoid.toPow 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 SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNSMul 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 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.toPow 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 IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction MulOpposite.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	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.toPow 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 SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNSMul ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.id	—	Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing fderiv_fun_pow differentiableAt_fun_id fderiv_id' IsSemitopologicalSemiring.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.toPow 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 IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction MulOpposite.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib ContinuousLinearMap.id	—	IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing SMulCommClass.opposite_mid IsScalarTower.right SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul fderiv_fun_pow' differentiableAt_fun_id fderiv_id' IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
hasFDerivAt_pow 📖	mathematical	—	HasFDerivAt 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.toPow 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 ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNSMul 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.toPow 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 IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction MulOpposite.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib ContinuousLinearMap.id	—	HasFDerivAt.pow' hasFDerivAt_id
hasFDerivWithinAt_pow 📖	mathematical	—	HasFDerivWithinAt 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.toPow 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 ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNSMul 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.toPow 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 IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction MulOpposite.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib ContinuousLinearMap.id	—	HasFDerivWithinAt.pow' hasFDerivWithinAt_id
hasStrictFDerivAt_pow 📖	mathematical	—	HasStrictFDerivAt 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.toPow 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 ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Algebra.to_smulCommClass Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing AddMonoid.toNSMul 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.toPow 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 IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing NonUnitalSeminormedRing.toIsTopologicalRing Finset.range MulOpposite ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MulOpposite.instMonoid ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction MulOpposite.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass IsScalarTower.right Semifield.toCommSemiring SeminormedRing.toRing NormedAlgebra.toAlgebra SeparatelyContinuousMul.to_continuousSMul_op IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring MulOpposite.op NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib ContinuousLinearMap.id	—	HasStrictFDerivAt.pow' hasStrictFDerivAt_id

---

← Back to Index