OAI/GroupTheory/PolycyclicRecognition/Geometry/SmoothRotationExtension.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual smooth graph and its compact extension

  1. instance OAI.PolycyclicRecognition.ComplexWeightFactorModel.smoothRotationExtensionTopologicalGroup line 22
  2. instance OAI.PolycyclicRecognition.ComplexWeightFactorModel.smoothRotationalModificationTopologicalGroup line 28
  3. def OAI.PolycyclicRecognition.ComplexWeightFactorModel.smoothRotationalModificationMetric line 33

    Source documentation

    The metric has exactly the existing graph topology.

    def smoothRotationalModificationMetric : MetricSpace (F.SmoothRotationalModification hExp) :=
…
  4. instance OAI.PolycyclicRecognition.ComplexWeightFactorModel.smoothRotationalModificationSimplyConnected line 37
  5. def OAI.PolycyclicRecognition.ComplexWeightFactorModel.originalToSmoothRotationExtension line 42
  6. def OAI.PolycyclicRecognition.ComplexWeightFactorModel.smoothModificationToRotationExtension line 48