OAI/NumberTheory/DukePrimeDegree/Geometry/RootPrefixLocalRestriction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Recovering prefix-box kernels from a larger open coordinate region

  1. theorem OAI.DukePrimeDegree.RootPrefixBox.restrict_box_eq_coordinateMeasure_restrict line 18
  2. theorem OAI.DukePrimeDegree.RootPrefixBox.restrict_eq_coordinateMeasure line 65