OAI/NumberTheory/DukePrimeDegree/Geometry/RootTransverseRectangles.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Product neighborhoods for the remaining-root transversals

  1. structure OAI.DukePrimeDegree.RootTransverseRectangle line 14
  2. def OAI.DukePrimeDegree.RootTransverseRectangle.inclusion line 25
  3. lemma OAI.DukePrimeDegree.RootTransverseRectangle.inclusion_isOpenEmbedding line 28
  4. theorem OAI.DukePrimeDegree.exists_shifted_root_rectangle line 36