Conformal

📁 Source: Mathlib/Geometry/Euclidean/Angle/Unoriented/Conformal.lean

Statistics

Metric	Count
Definitions Conformal	1
Theorems preserves_angle, preserves_angle	2
Total	3

InnerProductGeometry.ConformalAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preserves_angle 📖	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	InnerProductGeometry.angle DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.funLike	—	InnerProductGeometry.IsConformalMap.preserves_angle HasFDerivAt.unique IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace

InnerProductGeometry.IsConformalMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preserves_angle 📖	mathematical	IsConformalMap Real Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike	InnerProductGeometry.angle DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike	—	InnerProductGeometry.angle_smul_smul LinearIsometry.angle_map

(root)

Definitions

Name	Category	Theorems
Conformal 📖	MathDef	2 math math: conformal_const_smul, conformal_id

---

← Back to Index