OAI/NumberTheory/DukePrimeDegree/Geometry/RowSingleMeasure.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Coordinate measures of compatible row and root boxes

The actual coordinate measure of the one-root box is the coordinate change of the actual row-box measure. Consequently the abstract nested conditional compatibility applies to these restricted ambient measures.

  1. lemma OAI.DukePrimeDegree.RowRootBox.coordinateMeasure_apply line 20
  2. theorem OAI.DukePrimeDegree.singleRootBox_coordinateMeasure line 34
  3. lemma OAI.DukePrimeDegree.rowSingleMeasure_eq_map line 59
  4. theorem OAI.DukePrimeDegree.rowBox_root_conditional_compatibility line 66