OAI/NumberTheory/DukePrimeDegree/Geometry/NeutralUpperRootHomeomorph.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

An actual product chart with neutral translation as its final factor

  1. lemma OAI.DukePrimeDegree.upperRootDilation_opposite_cancel line 14
  2. def OAI.DukePrimeDegree.neutralRootSkewHomeomorph line 24
  3. def OAI.DukePrimeDegree.neutralUpperRootHomeomorph line 43
  4. lemma OAI.DukePrimeDegree.neutralUpperRootHomeomorph_apply line 53
  5. lemma OAI.DukePrimeDegree.isOpen_positiveTransverse line 59
  6. lemma OAI.DukePrimeDegree.neutralUpperRootParam_isOpenEmbedding line 66
  7. lemma OAI.DukePrimeDegree.neutralUpperRootQuotientParam_localHomeomorph line 78