OAI/NumberTheory/DukePrimeDegree/Geometry/NeutralCoordinateMeasure.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Translation invariance in the actual neutral product chart

  1. theorem OAI.DukePrimeDegree.comap_map_eq_of_equivariant line 15
  2. abbrev OAI.DukePrimeDegree.NeutralCoordinateBase line 39
  3. def OAI.DukePrimeDegree.neutralProductParam line 41
  4. lemma OAI.DukePrimeDegree.neutralProductParam_isOpenEmbedding line 45
  5. lemma OAI.DukePrimeDegree.neutralProductParam_add line 50
  6. def OAI.DukePrimeDegree.neutralCoordinateMeasure line 56
  7. lemma OAI.DukePrimeDegree.neutralCoordinateBase_locallyCompact line 60
  8. lemma OAI.DukePrimeDegree.neutralCoordinateBase_secondCountable line 67
  9. theorem OAI.DukePrimeDegree.neutralCoordinateMeasure_finiteOnCompacts line 74
  10. theorem OAI.DukePrimeDegree.neutralCoordinateMeasure_translation line 84