OAI/NumberTheory/DukePrimeDegree/Geometry/RowSingleBox.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Compatible row and one-root boxes

For a row box with cubical time domain, separating any one root gives an actual one-root box. The quotient parametrizations agree on their domains, not merely up to a leaf-equivalence relation.

  1. def OAI.DukePrimeDegree.rowToSingleHomeomorph line 21
  2. lemma OAI.DukePrimeDegree.rowToSingleHomeomorph_apply line 27
  3. theorem OAI.DukePrimeDegree.rowToSingleHomeomorph_param line 32
  4. lemma OAI.DukePrimeDegree.rowCube_member_split line 41
  5. def OAI.DukePrimeDegree.rowSingleTransverse line 48
  6. lemma OAI.DukePrimeDegree.rowToSingle_domain line 52
  7. def OAI.DukePrimeDegree.RowRootBox.singleRootBox line 65