OAI/NumberTheory/DukePrimeDegree/Geometry/ShiftedRootPullback.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Actual coordinate measures for root charts with varying time origins

  1. def OAI.DukePrimeDegree.realFiberShift line 16
  2. def OAI.DukePrimeDegree.shiftedRootFactorCoordinateMap line 25
  3. lemma OAI.DukePrimeDegree.shiftedRootFactorCoordinateMap_embedding line 29
  4. def OAI.DukePrimeDegree.shiftedRootFactorPullback line 35
  5. lemma OAI.DukePrimeDegree.shiftedRootFactorPullback_finite line 40
  6. lemma OAI.DukePrimeDegree.shiftedRootFactorPullback_map line 52