OAI/NumberTheory/DukePrimeDegree/Geometry/RootPrefixLift.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Root-prefix box measures agree with the actual covering lift

  1. def OAI.DukePrimeDegree.RootPrefixCoordinates.timeGroupParam line 18
  2. theorem OAI.DukePrimeDegree.RootPrefixCoordinates.timeGroupParam_isOpenEmbedding line 23
  3. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.quotient_timeGroupParam line 33
  4. theorem OAI.DukePrimeDegree.RootPrefixBox.coordinateMeasure_eq_lift_restrict line 48