OAI/NumberTheory/DukePrimeDegree/Geometry/ProjectiveLeafEquality.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Removing the projective scalar after changing a leaf's origin

  1. theorem OAI.DukePrimeDegree.anchorNormalize_eq_of_basedRealMeasure_eq line 14
  2. theorem OAI.DukePrimeDegree.anchorNormalize_eq_of_rebasedRealMeasure_eq line 36
  3. lemma OAI.DukePrimeDegree.translatedRealMeasure_locallyFinite line 57
  4. lemma OAI.DukePrimeDegree.translatedRealMeasure_ball line 66
  5. theorem OAI.DukePrimeDegree.anchorNormalize_eq_of_shifted_rebasedRealMeasure_eq line 70