OAI/NumberTheory/DukePrimeDegree/Geometry/PhysicalPrefixCoordinates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Physical rectangles in the original remaining-subgroup time chart

  1. def OAI.DukePrimeDegree.RootPrefixCoordinates.remainingFactorTime line 17
  2. def OAI.DukePrimeDegree.RootPrefixCoordinates.physicalPrefixCoordinates line 21
  3. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.physicalPrefixCoordinates_param line 30
  4. def OAI.DukePrimeDegree.RootPrefixCoordinates.originalRectangleCoordinates line 45
  5. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.originalRectangleCoordinates_openEmbedding line 50
  6. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.originalRectangleCoordinates_param line 56
  7. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.originalRectangleCoordinates_image line 64