OAI/NumberTheory/DukePrimeDegree/Geometry/RootPrefixCoordinates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Coordinates with the processed roots before the remaining subgroup

These coordinates keep the remaining subgroup on the right, so its fibers are actual right orbits at every step of the product induction.

  1. structure OAI.DukePrimeDegree.RootPrefixCoordinates line 18
  2. def OAI.DukePrimeDegree.RootPrefixCoordinates.empty line 28
  3. def OAI.DukePrimeDegree.RootPrefixCoordinates.extend line 39
  4. def OAI.DukePrimeDegree.RootPrefixCoordinates.groupParam line 69
  5. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.groupParam_eq_mul line 73
  6. theorem OAI.DukePrimeDegree.RootPrefixCoordinates.groupParam_isOpenEmbedding line 81
  7. def OAI.DukePrimeDegree.RootPrefixCoordinates.quotientParam line 87
  8. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.quotientParam_eq_action line 91
  9. theorem OAI.DukePrimeDegree.RootPrefixCoordinates.quotientParam_localHomeomorph line 102