OAI/NumberTheory/DukePrimeDegree/Geometry/RootPrefixBoxes.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Actual quotient boxes for every remaining root subgroup

  1. def OAI.DukePrimeDegree.RootPrefixCoordinates.timeParam line 18
  2. lemma OAI.DukePrimeDegree.RootPrefixCoordinates.timeParam_eq_action line 23
  3. theorem OAI.DukePrimeDegree.RootPrefixCoordinates.timeParam_localHomeomorph line 30
  4. structure OAI.DukePrimeDegree.RootPrefixBox line 40
  5. theorem OAI.DukePrimeDegree.exists_rootPrefixBox_at_coordinates line 51
  6. abbrev OAI.DukePrimeDegree.RootPrefixBox.domain line 70
  7. abbrev OAI.DukePrimeDegree.RootPrefixBox.param line 71
  8. def OAI.DukePrimeDegree.RootPrefixBox.range line 73
  9. lemma OAI.DukePrimeDegree.RootPrefixBox.range_open line 76
  10. def OAI.DukePrimeDegree.RootPrefixBox.coordinateMeasure line 78
  11. instance OAI.DukePrimeDegree.RootPrefixBox.coordinateMeasure_finite line 82
  12. lemma OAI.DukePrimeDegree.RootPrefixBox.map_coordinateMeasure line 91
  13. def OAI.DukePrimeDegree.RootPrefixBox.conditionalKernel line 98
  14. instance OAI.DukePrimeDegree.RootPrefixBox.conditionalKernel_markov line 102
  15. theorem OAI.DukePrimeDegree.RootPrefixBox.disintegrate line 107