OAI/Analysis/JiangSu/DimensionDrop/ConcreteLimit.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.JiangSuConstruction.PositivePair line 14
  2. def OAI.JiangSuConstruction.PositivePair.next line 20
  3. def OAI.JiangSuConstruction.stagePair line 24
  4. lemma OAI.JiangSuConstruction.stagePair_prime_powers line 28
  5. lemma OAI.JiangSuConstruction.stagePair_coprime line 40
  6. abbrev OAI.JiangSuConstruction.StageAlgebra line 45
  7. instance OAI.JiangSuConstruction.stageAlgebraNontrivial line 50
  8. def OAI.JiangSuConstruction.stageStep line 55
  9. lemma OAI.JiangSuConstruction.stageStep_injective line 57
  10. def OAI.JiangSuConstruction.concreteSystem line 60
  11. abbrev OAI.JiangSuConstruction.PrimeDropLimit line 63
  12. instance OAI.JiangSuConstruction.primeDropLimitNontrivial line 65
  13. theorem OAI.JiangSuConstruction.primeDropLimit_finite_stage line 68