OAI/NumberTheory/DukePrimeDegree/Geometry/RootPrefixRegularKernel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Everywhere locally finite versions of remaining-subgroup kernels

  1. def OAI.DukePrimeDegree.finiteRemainingCubes line 16
  2. lemma OAI.DukePrimeDegree.measurableSet_finiteRemainingCubes line 20
  3. lemma OAI.DukePrimeDegree.locallyFinite_of_finite_remainingCubes line 27
  4. def OAI.DukePrimeDegree.locallyFiniteRemainingVersion line 36
  5. lemma OAI.DukePrimeDegree.locallyFiniteRemainingVersion_eq line 40
  6. instance OAI.DukePrimeDegree.locallyFiniteRemainingVersion_locallyFinite line 47
  7. instance OAI.DukePrimeDegree.locallyFiniteRemainingVersion_sFinite line 55
  8. def OAI.DukePrimeDegree.RootPrefixBox.regularLeafKernel line 71
  9. instance OAI.DukePrimeDegree.RootPrefixBox.regularLeafKernel_locallyFinite line 78
  10. instance OAI.DukePrimeDegree.RootPrefixBox.regularLeafKernel_sFinite line 86
  11. lemma OAI.DukePrimeDegree.RootPrefixBox.ae_regularLeafKernel_eq line 93