InnerProduct

📁 Source: Mathlib/Analysis/Calculus/Conformal/InnerProduct.lean

Statistics

Metric	Count
Definitions conformalFactorAt	1
Theorems conformalAt_iff, conformalAt_iff', conformalFactorAt_inner_eq_mul_inner, conformalFactorAt_inner_eq_mul_inner', conformalFactorAt_pos	5
Total	6

(root)

Definitions

Name	Category	Theorems
conformalFactorAt 📖	CompOp	3 math math: conformalFactorAt_inner_eq_mul_inner', conformalFactorAt_pos, conformalFactorAt_inner_eq_mul_inner

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conformalAt_iff 📖	mathematical	HasFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	ConformalAt Real.instLT Real.instZero Inner.inner InnerProductSpace.toInner DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.funLike Real.instMul	—	HasFDerivAt.fderiv IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
conformalAt_iff' 📖	mathematical	—	ConformalAt InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Real.instLT Real.instZero Inner.inner InnerProductSpace.toInner DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike fderiv Real.instMul	—	conformalAt_iff_isConformalMap_fderiv isConformalMap_iff
conformalFactorAt_inner_eq_mul_inner 📖	mathematical	HasFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ConformalAt	Inner.inner InnerProductSpace.toInner DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.funLike Real.instMul conformalFactorAt	—	conformalFactorAt_inner_eq_mul_inner' HasFDerivAt.unique IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace DifferentiableAt.hasFDerivAt ConformalAt.differentiableAt
conformalFactorAt_inner_eq_mul_inner' 📖	mathematical	ConformalAt InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup	Inner.inner InnerProductSpace.toInner DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike fderiv Real.instMul conformalFactorAt	—	conformalAt_iff'
conformalFactorAt_pos 📖	mathematical	ConformalAt InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup	Real.instLT Real.instZero conformalFactorAt	—	conformalAt_iff'

---

← Back to Index