OAI/NumberTheory/DukePrimeDegree/Geometry/UpperRootRegularKernel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Everywhere locally finite versions of full upper-root kernels

  1. def OAI.DukePrimeDegree.finiteUpperRootCubes line 14
  2. lemma OAI.DukePrimeDegree.measurableSet_finiteUpperRootCubes line 18
  3. lemma OAI.DukePrimeDegree.locallyFinite_of_finite_upperRootCubes line 25
  4. def OAI.DukePrimeDegree.locallyFiniteUpperRootVersion line 34
  5. lemma OAI.DukePrimeDegree.locallyFiniteUpperRootVersion_eq line 38
  6. instance OAI.DukePrimeDegree.locallyFiniteUpperRootVersion_locallyFinite line 45
  7. instance OAI.DukePrimeDegree.locallyFiniteUpperRootVersion_sFinite line 53
  8. def OAI.DukePrimeDegree.UpperRootBox.regularLeafKernel line 66
  9. instance OAI.DukePrimeDegree.UpperRootBox.regularLeafKernel_locallyFinite line 73
  10. instance OAI.DukePrimeDegree.UpperRootBox.regularLeafKernel_sFinite line 81
  11. lemma OAI.DukePrimeDegree.UpperRootBox.ae_regularLeafKernel_eq line 88