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 NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ConformalAt	InnerProductGeometry.angle DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike 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 Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike ContinuousLinearMap.funLike	—	InnerProductGeometry.angle_smul_smul LinearIsometry.angle_map

(root)

Definitions

Name	Category	Theorems
Conformal 📖	MathDef	4 math math: conformal_const_smul, Conformal.const_smul, conformal_id, Conformal.comp

---

← Back to Index