OAI/NumberTheory/DukePrimeDegree/Geometry/RemainingProductDiagonal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Diagonal covariance in actual remaining-root time coordinates

  1. lemma OAI.DukePrimeDegree.EliminationChain.remainingEuclideanCoordinates_dilation line 17
  2. lemma OAI.DukePrimeDegree.EliminationChain.remainingTimeProduct_eq_map line 31
  3. lemma OAI.DukePrimeDegree.EliminationChain.remainingCoordinates_unit_cube line 45
  4. theorem OAI.DukePrimeDegree.EliminationChain.ae_remainingTimeProduct_diagonal line 65