OAI/NumberTheory/DukePrimeDegree/Geometry/RemainingProjectiveEquality.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Recovering a prefix conditional from its based group measure

  1. lemma OAI.DukePrimeDegree.EliminationChain.centeredRemainingMeasure_unit_lt_top line 15
  2. lemma OAI.DukePrimeDegree.EliminationChain.uncenter_basedRemainingGroupMeasure line 24
  3. theorem OAI.DukePrimeDegree.EliminationChain.anchorNormalize_of_basedRemainingGroupMeasure line 49
  4. theorem OAI.DukePrimeDegree.EliminationChain.uncenter_basedRemainingGroupMeasure_mass line 62
  5. theorem OAI.DukePrimeDegree.RootPrefixBox.conditional_of_based_group_measure line 83
  6. theorem OAI.DukePrimeDegree.RootPrefixBox.based_group_measure_uncenter_mass line 106