OAI/NumberTheory/DukePrimeDegree/Geometry/NextProductTranslations.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Translated intrinsic products in the extended-prefix time coordinates

  1. lemma OAI.DukePrimeDegree.InitialRootStep.nextGroupCast_mul line 14
  2. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.translated_nextProduct_time_coordinates line 25
  3. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.normalized_nextProduct_time_coordinates line 44