OAI/NumberTheory/DukePrimeDegree/Geometry/RemainingRebase.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Rebasing a remaining-subgroup leaf at its current coordinate

  1. def OAI.DukePrimeDegree.EliminationChain.remainingRebase line 16
  2. lemma OAI.DukePrimeDegree.EliminationChain.remainingRebase_word line 22
  3. lemma OAI.DukePrimeDegree.EliminationChain.continuous_remainingRebase line 28
  4. lemma OAI.DukePrimeDegree.EliminationChain.remainingWord_zero line 35
  5. lemma OAI.DukePrimeDegree.EliminationChain.remainingRebase_self line 41
  6. lemma OAI.DukePrimeDegree.EliminationChain.remainingRebase_cocycle line 47
  7. def OAI.DukePrimeDegree.EliminationChain.centeredRemainingMeasure line 55
  8. lemma OAI.DukePrimeDegree.EliminationChain.centeredRemainingMeasure_locallyFinite line 59
  9. lemma OAI.DukePrimeDegree.EliminationChain.centeredRemainingMeasure_unit_pos line 73
  10. def OAI.DukePrimeDegree.EliminationChain.basedRemainingMeasure line 84
  11. lemma OAI.DukePrimeDegree.EliminationChain.basedRemainingMeasure_unit line 88
  12. lemma OAI.DukePrimeDegree.EliminationChain.basedRemainingMeasure_locallyFinite line 99