OAI/NumberTheory/DukePrimeDegree/Geometry/NextGroupCoordinates.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Entry-coordinate homeomorphism for the next remaining root group

  1. lemma OAI.DukePrimeDegree.InitialRootStep.next_initial line 15
  2. lemma OAI.DukePrimeDegree.InitialRootStep.next_closed line 18
  3. lemma OAI.DukePrimeDegree.InitialRootStep.exists_nextGroupCoordinates line 24
  4. def OAI.DukePrimeDegree.InitialRootStep.nextGroupCoordinates line 38
  5. lemma OAI.DukePrimeDegree.InitialRootStep.nextGroupCoordinates_apply line 42