Calculus

📁 Source: Mathlib/Analysis/InnerProductSpace/Calculus.lean

Statistics

Metric	Count
Definitions fderivInnerCLM	1
Theorems dist, inner, norm, norm_sq, dist, inner, norm, norm_sq, dist, inner, norm, norm_sq, dist, inner, norm, norm_sq, dist, inner, norm, norm_sq, dist, inner, norm, norm_sq, dist, inner, norm, norm_sq, dist, inner, norm, norm_sq, inner, norm_sq, inner, norm_sq, inner, norm_sq, inner, norm_sq, inner, contDiff_unitBall, contDiffOn_univBall_symm, contDiffOn_univUnitBall_symm, contDiff_unitBallBall, contDiff_unitBallBall_symm, contDiff_univBall, contDiff_univUnitBall, contDiffAt_euclidean, contDiffAt_inner, contDiffAt_norm, contDiffOn_euclidean, contDiffWithinAt_euclidean, contDiff_euclidean, contDiff_inner, contDiff_norm_sq, deriv_inner_apply, differentiableAt_euclidean, differentiableOn_euclidean, differentiableWithinAt_euclidean, differentiable_euclidean, differentiable_inner, fderivInnerCLM_apply, fderiv_inner_apply, fderiv_norm_sq, fderiv_norm_sq_apply, hasFDerivWithinAt_euclidean, hasStrictFDerivAt_euclidean, hasStrictFDerivAt_norm_sq	69
Total	70

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist 📖	mathematical	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace	—	contDiff_iff_contDiffAt ContDiffAt.dist contDiffAt
inner 📖	mathematical	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Inner.inner InnerProductSpace.toInner	—	comp contDiff_inner prodMk
norm 📖	mathematical	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Norm.norm NormedAddCommGroup.toNorm	—	contDiff_iff_contDiffAt ContDiffAt.norm contDiffAt
norm_sq 📖	mathematical	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm	—	comp contDiff_norm_sq

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist 📖	mathematical	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace	—	dist_eq_norm norm sub sub_ne_zero
inner 📖	mathematical	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Inner.inner InnerProductSpace.toInner	—	ContDiffWithinAt.inner
norm 📖	mathematical	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Norm.norm NormedAddCommGroup.toNorm	—	comp contDiffAt_norm
norm_sq 📖	mathematical	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm	—	ContDiffWithinAt.norm_sq

ContDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist 📖	mathematical	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace	—	ContDiffWithinAt.dist
inner 📖	mathematical	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Inner.inner InnerProductSpace.toInner	—	ContDiffWithinAt.inner
norm 📖	mathematical	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Norm.norm NormedAddCommGroup.toNorm	—	ContDiffWithinAt.norm
norm_sq 📖	mathematical	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm	—	ContDiffWithinAt.norm_sq

ContDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist 📖	mathematical	ContDiffWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace	—	dist_eq_norm norm sub sub_ne_zero
inner 📖	mathematical	ContDiffWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Inner.inner InnerProductSpace.toInner	—	ContDiffAt.comp_contDiffWithinAt contDiffAt_inner prodMk
norm 📖	mathematical	ContDiffWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Norm.norm NormedAddCommGroup.toNorm	—	ContDiffAt.comp_contDiffWithinAt contDiffAt_norm
norm_sq 📖	mathematical	ContDiffWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm	—	ContDiffAt.comp_contDiffWithinAt ContDiff.contDiffAt contDiff_norm_sq

Differentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist 📖	mathematical	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace Dist.dist PseudoMetricSpace.toDist	—	DifferentiableAt.dist
inner 📖	mathematical	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Inner.inner InnerProductSpace.toInner	—	DifferentiableAt.inner
norm 📖	mathematical	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace Norm.norm NormedAddCommGroup.toNorm	—	DifferentiableAt.norm
norm_sq 📖	mathematical	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm	—	DifferentiableAt.norm_sq

DifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist 📖	mathematical	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace Dist.dist PseudoMetricSpace.toDist	—	dist_eq_norm norm sub sub_ne_zero
inner 📖	mathematical	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Inner.inner InnerProductSpace.toInner	—	HasFDerivAt.differentiableAt RingHomCompTriple.ids HasFDerivAt.inner hasFDerivAt
norm 📖	mathematical	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace Norm.norm NormedAddCommGroup.toNorm	—	comp ContDiffAt.differentiableAt contDiffAt_norm one_ne_zero NeZero.charZero_one WithTop.charZero
norm_sq 📖	mathematical	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm	—	comp ContDiffAt.differentiableAt ContDiffAt.norm_sq contDiffAt_id one_ne_zero NeZero.charZero_one WithTop.charZero

DifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist 📖	mathematical	DifferentiableOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace Dist.dist PseudoMetricSpace.toDist	—	DifferentiableWithinAt.dist
inner 📖	mathematical	DifferentiableOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Inner.inner InnerProductSpace.toInner	—	DifferentiableWithinAt.inner
norm 📖	mathematical	DifferentiableOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace Norm.norm NormedAddCommGroup.toNorm	—	DifferentiableWithinAt.norm
norm_sq 📖	mathematical	DifferentiableOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm	—	DifferentiableWithinAt.norm_sq

DifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist 📖	mathematical	DifferentiableWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace Dist.dist PseudoMetricSpace.toDist	—	dist_eq_norm norm sub sub_ne_zero
inner 📖	mathematical	DifferentiableWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Inner.inner InnerProductSpace.toInner	—	HasFDerivWithinAt.differentiableWithinAt RingHomCompTriple.ids HasFDerivWithinAt.inner hasFDerivWithinAt
norm 📖	mathematical	DifferentiableWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace Norm.norm NormedAddCommGroup.toNorm	—	DifferentiableAt.comp_differentiableWithinAt ContDiffAt.differentiableAt ContDiffAt.norm contDiffAt_id one_ne_zero NeZero.charZero_one WithTop.charZero
norm_sq 📖	mathematical	DifferentiableWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm	—	DifferentiableAt.comp_differentiableWithinAt ContDiffAt.differentiableAt ContDiffAt.norm_sq contDiffAt_id one_ne_zero NeZero.charZero_one WithTop.charZero

HasDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner 📖	mathematical	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul	NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Inner.inner InnerProductSpace.toInner Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasDerivWithinAt.inner
norm_sq 📖	mathematical	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul	Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing Real.instAdd IsTopologicalSemiring.toIsModuleTopology Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Inner.inner InnerProductSpace.toInner	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal RingHomIsometric.ids RingHomCompTriple.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul Nat.instAtLeastTwoHAddOfNat congr_simp nsmul_eq_mul one_smul HasFDerivAt.hasDerivAt HasFDerivAt.norm_sq hasFDerivAt

HasDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner 📖	mathematical	HasDerivWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul	NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Inner.inner InnerProductSpace.toInner Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul RingHomCompTriple.ids congr_simp one_smul HasFDerivWithinAt.hasDerivWithinAt HasFDerivWithinAt.inner hasFDerivWithinAt
norm_sq 📖	mathematical	HasDerivWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul	Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing Real.instAdd IsTopologicalSemiring.toIsModuleTopology Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Inner.inner InnerProductSpace.toInner	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal RingHomIsometric.ids RingHomCompTriple.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul Nat.instAtLeastTwoHAddOfNat congr_simp nsmul_eq_mul one_smul HasFDerivWithinAt.hasDerivWithinAt HasFDerivWithinAt.norm_sq hasFDerivWithinAt

HasFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner 📖	mathematical	HasFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Inner.inner InnerProductSpace.toInner ContinuousLinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instTopologicalSpaceProd Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Prod.instModule RingHomCompTriple.ids fderivInnerCLM ContinuousLinearMap.prod	—	comp isBoundedBilinearMap_inner Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace IsBoundedBilinearMap.hasFDerivAt prodMk
norm_sq 📖	mathematical	HasFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace InnerProductSpace.toNormedSpace Real.instRCLike	NormedAddCommGroup.toAddCommGroup Real.instAddCommGroup DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.innerProductSpace Real.pseudoMetricSpace Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm ContinuousLinearMap Real.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid ContinuousLinearMap.toNormedAddCommGroup Real.normedAddCommGroup RCLike.toInnerProductSpaceReal RingHomIsometric.ids Real.normedCommRing ESeminormedAddCommMonoid.toESeminormedAddMonoid ContinuousLinearMap.comp RingHomCompTriple.ids DFunLike.coe CommSemiring.toSemiring Semifield.toCommSemiring starRingEnd RCLike.toStarRing ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.module Algebra.to_smulCommClass Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousLinearMap.funLike innerSL	—	comp RingHomIsometric.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul HasStrictFDerivAt.hasFDerivAt hasStrictFDerivAt_norm_sq

HasFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner 📖	mathematical	HasFDerivWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Inner.inner InnerProductSpace.toInner ContinuousLinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instTopologicalSpaceProd Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Prod.instModule RingHomCompTriple.ids fderivInnerCLM ContinuousLinearMap.prod	—	HasFDerivAt.comp_hasFDerivWithinAt isBoundedBilinearMap_inner Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace IsBoundedBilinearMap.hasFDerivAt prodMk
norm_sq 📖	mathematical	HasFDerivWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace InnerProductSpace.toNormedSpace Real.instRCLike	NormedAddCommGroup.toAddCommGroup Real.instAddCommGroup DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.innerProductSpace Real.pseudoMetricSpace Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm ContinuousLinearMap Real.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid ContinuousLinearMap.toNormedAddCommGroup Real.normedAddCommGroup RCLike.toInnerProductSpaceReal RingHomIsometric.ids Real.normedCommRing ESeminormedAddCommMonoid.toESeminormedAddMonoid ContinuousLinearMap.comp RingHomCompTriple.ids DFunLike.coe CommSemiring.toSemiring Semifield.toCommSemiring starRingEnd RCLike.toStarRing ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.module Algebra.to_smulCommClass Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousLinearMap.funLike innerSL	—	HasFDerivAt.comp_hasFDerivWithinAt RingHomIsometric.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul HasStrictFDerivAt.hasFDerivAt hasStrictFDerivAt_norm_sq

HasStrictFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner 📖	mathematical	HasStrictFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Inner.inner InnerProductSpace.toInner ContinuousLinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instTopologicalSpaceProd Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Prod.instModule RingHomCompTriple.ids fderivInnerCLM ContinuousLinearMap.prod	—	comp isBoundedBilinearMap_inner Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace IsBoundedBilinearMap.hasStrictFDerivAt prodMk

Homeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiff_unitBall 📖	mathematical	—	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop.some ENat Set Set.instMembership Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instOne DFunLike.coe Homeomorph Set.Elem UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instTopologicalSpaceSubtype EquivLike.toFunLike instEquivLike unitBall	—	OpenPartialHomeomorph.contDiff_univUnitBall

OpenPartialHomeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffOn_univBall_symm 📖	mathematical	—	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop.some ENat toFun' UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace symm univBall SeminormedAddCommGroup.toNormedAddTorsor Metric.ball	—	ContDiffOn.comp contDiffOn_univUnitBall_symm ContDiff.contDiffOn contDiff_unitBallBall_symm unitBallBall_source unitBallBall_target symm_mapsTo ContDiffOn.sub contDiffOn_id contDiffOn_const
contDiffOn_univUnitBall_symm 📖	mathematical	—	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop.some ENat toFun' UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace symm univUnitBall Metric.ball NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real.instOne	—	ContDiffAt.contDiffWithinAt sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid one_pow sq_lt_sq Real.instIsStrictOrderedRing abs_norm abs_one Real.instIsOrderedRing mem_ball_zero_iff ContDiffAt.inv ContDiffAt.comp Real.contDiffAt_sqrt LT.lt.ne' ContDiffAt.sub contDiffAt_const ContDiff.contDiffAt contDiff_norm_sq Real.sqrt_ne_zero' ContDiffAt.smul NormedSpace.toIsBoundedSMul IsScalarTower.left contDiffAt_id
contDiff_unitBallBall 📖	mathematical	Real Real.instLT Real.instZero	ContDiff DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop.some ENat toFun' UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace unitBallBall SeminormedAddCommGroup.toNormedAddTorsor	—	ContDiff.add ContDiff.const_smul smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul contDiff_id contDiff_const
contDiff_unitBallBall_symm 📖	mathematical	Real Real.instLT Real.instZero	ContDiff DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop.some ENat toFun' UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace symm unitBallBall SeminormedAddCommGroup.toNormedAddTorsor	—	ContDiff.const_smul smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContDiff.sub contDiff_id contDiff_const
contDiff_univBall 📖	mathematical	—	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop.some ENat toFun' UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace univBall SeminormedAddCommGroup.toNormedAddTorsor	—	ContDiff.comp contDiff_unitBallBall contDiff_univUnitBall ContDiff.add contDiff_id contDiff_const
contDiff_univUnitBall 📖	mathematical	—	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop.some ENat toFun' UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace univUnitBall	—	add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing Real.instIsStrictOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul ContDiff.inv ContDiff.sqrt ContDiff.add contDiff_const contDiff_norm_sq LT.lt.ne' Real.sqrt_ne_zero' ContDiff.smul NormedSpace.toIsBoundedSMul IsScalarTower.left contDiff_id

(root)

Definitions

Name	Category	Theorems
fderivInnerCLM 📖	CompOp	4 math math: HasFDerivWithinAt.inner, HasFDerivAt.inner, HasStrictFDerivAt.inner, fderivInnerCLM_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffAt_euclidean 📖	mathematical	—	ContDiffAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField EuclideanSpace PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField PiLp.normedSpace NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace NormedAddCommGroup.toSeminormedAddCommGroup WithLp.ofLp	—	contDiffAt_piLp fact_one_le_two_ennreal
contDiffAt_inner 📖	mathematical	—	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Inner.inner InnerProductSpace.toInner	—	ContDiff.contDiffAt contDiff_inner
contDiffAt_norm 📖	mathematical	—	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Norm.norm NormedAddCommGroup.toNorm	—	pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass LT.lt.ne' norm_pos_iff Real.sqrt_sq ContDiffAt.sqrt ContDiffAt.norm_sq contDiffAt_id
contDiffOn_euclidean 📖	mathematical	—	ContDiffOn DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField EuclideanSpace PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField PiLp.normedSpace NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace NormedAddCommGroup.toSeminormedAddCommGroup WithLp.ofLp	—	contDiffOn_piLp fact_one_le_two_ennreal
contDiffWithinAt_euclidean 📖	mathematical	—	ContDiffWithinAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField EuclideanSpace PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField PiLp.normedSpace NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace NormedAddCommGroup.toSeminormedAddCommGroup WithLp.ofLp	—	contDiffWithinAt_piLp fact_one_le_two_ennreal
contDiff_euclidean 📖	mathematical	—	ContDiff DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField EuclideanSpace PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField PiLp.normedSpace NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace NormedAddCommGroup.toSeminormedAddCommGroup WithLp.ofLp	—	contDiff_piLp fact_one_le_two_ennreal
contDiff_inner 📖	mathematical	—	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Inner.inner InnerProductSpace.toInner	—	IsBoundedBilinearMap.contDiff isBoundedBilinearMap_inner Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
contDiff_norm_sq 📖	mathematical	—	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm	—	inner_self_eq_norm_sq ContDiff.comp ContinuousLinearMap.contDiff ContDiff.inner contDiff_id
deriv_inner_apply 📖	mathematical	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace	deriv NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Inner.inner InnerProductSpace.toInner Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing	—	HasDerivAt.deriv HasDerivAt.inner DifferentiableAt.hasDerivAt
differentiableAt_euclidean 📖	mathematical	—	DifferentiableAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace EuclideanSpace WithLp.instAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Pi.addCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing WithLp.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace PiLp.topologicalSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing WithLp.ofLp	—	differentiableAt_piLp fact_one_le_two_ennreal
differentiableOn_euclidean 📖	mathematical	—	DifferentiableOn DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace EuclideanSpace WithLp.instAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Pi.addCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing WithLp.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace PiLp.topologicalSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing WithLp.ofLp	—	differentiableOn_piLp fact_one_le_two_ennreal
differentiableWithinAt_euclidean 📖	mathematical	—	DifferentiableWithinAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace EuclideanSpace WithLp.instAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Pi.addCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing WithLp.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace PiLp.topologicalSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing WithLp.ofLp	—	differentiableWithinAt_piLp fact_one_le_two_ennreal
differentiable_euclidean 📖	mathematical	—	Differentiable DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace EuclideanSpace WithLp.instAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Pi.addCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing WithLp.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace PiLp.topologicalSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing WithLp.ofLp	—	differentiable_piLp fact_one_le_two_ennreal
differentiable_inner 📖	mathematical	—	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup Prod.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField instTopologicalSpaceProd NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing Inner.inner InnerProductSpace.toInner	—	IsBoundedBilinearMap.differentiableAt isBoundedBilinearMap_inner Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
fderivInnerCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Prod.instModule NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal ContinuousLinearMap.funLike fderivInnerCLM Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Inner.inner InnerProductSpace.toInner	—	—
fderiv_inner_apply 📖	mathematical	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal ContinuousLinearMap.funLike fderiv Inner.inner InnerProductSpace.toInner Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing	—	RingHomCompTriple.ids HasFDerivAt.fderiv IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace HasFDerivAt.inner DifferentiableAt.hasFDerivAt
fderiv_norm_sq 📖	mathematical	—	fderiv Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm AddMonoid.toNatSMul Pi.addMonoid ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing RCLike.innerProductSpace ESeminormedAddMonoid.toAddMonoid ContinuousLinearMap.toNormedAddCommGroup Real.normedAddCommGroup RingHomIsometric.ids ESeminormedAddCommMonoid.toESeminormedAddMonoid DFunLike.coe CommSemiring.toSemiring Semifield.toCommSemiring starRingEnd RCLike.toStarRing ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.module Algebra.to_smulCommClass Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousLinearMap.funLike innerSL	—	RingHomIsometric.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul fderiv_norm_sq_apply
fderiv_norm_sq_apply 📖	mathematical	—	fderiv Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing RCLike.innerProductSpace NontriviallyNormedField.toNormedField AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid ContinuousLinearMap.toNormedAddCommGroup Real.normedAddCommGroup RingHomIsometric.ids ESeminormedAddCommMonoid.toESeminormedAddMonoid DFunLike.coe CommSemiring.toSemiring Semifield.toCommSemiring starRingEnd RCLike.toStarRing ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.module Algebra.to_smulCommClass Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousLinearMap.funLike innerSL	—	HasFDerivAt.fderiv RingHomIsometric.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul instIsTopologicalRingReal IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace HasStrictFDerivAt.hasFDerivAt hasStrictFDerivAt_norm_sq
hasFDerivWithinAt_euclidean 📖	mathematical	—	HasFDerivWithinAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace EuclideanSpace WithLp.instAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Pi.addCommGroup NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing WithLp.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace PiLp.topologicalSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing WithLp.ofLp ContinuousLinearMap.comp NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid RingHomCompTriple.ids PiLp.proj	—	hasFDerivWithinAt_piLp fact_one_le_two_ennreal
hasStrictFDerivAt_euclidean 📖	mathematical	—	HasStrictFDerivAt DenselyNormedField.toNontriviallyNormedField RCLike.toDenselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace EuclideanSpace WithLp.instAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Pi.addCommGroup NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing WithLp.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace PiLp.topologicalSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing WithLp.ofLp ContinuousLinearMap.comp NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid RingHomCompTriple.ids PiLp.proj	—	hasStrictFDerivAt_piLp fact_one_le_two_ennreal
hasStrictFDerivAt_norm_sq 📖	mathematical	—	HasStrictFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule DenselyNormedField.toNormedField RCLike.toDenselyNormedField Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing RCLike.innerProductSpace Real.pseudoMetricSpace Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NontriviallyNormedField.toNormedField AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid ContinuousLinearMap.toNormedAddCommGroup Real.normedAddCommGroup RCLike.toInnerProductSpaceReal RingHomIsometric.ids Real.normedCommRing ESeminormedAddCommMonoid.toESeminormedAddMonoid DFunLike.coe CommSemiring.toSemiring Semifield.toCommSemiring starRingEnd RCLike.toStarRing ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.module Algebra.to_smulCommClass Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousLinearMap.funLike innerSL	—	RingHomIsometric.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul sq inner_self_eq_norm_mul_norm RingHomCompTriple.ids ContinuousLinearMap.ext instIsTopologicalRingReal two_smul real_inner_comm HasStrictFDerivAt.inner hasStrictFDerivAt_id

---

← Back to Index