OAI/RingTheory/Kurosh/ScheduledTowers.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Countable towers with scheduled algebraicity requirements and growing degree.

  1. def OAI.KuroshConstruction.stageEnumeration line 10
  2. lemma OAI.KuroshConstruction.stageEnumeration_surjective line 19
  3. structure OAI.KuroshConstruction.ScheduledState line 29
  4. def OAI.KuroshConstruction.initialScheduledState line 33
  5. def OAI.KuroshConstruction.nextScheduledStage line 36
  6. def OAI.KuroshConstruction.nextScheduledStep line 41
  7. def OAI.KuroshConstruction.nextScheduledState line 47
  8. def OAI.KuroshConstruction.scheduledSequence line 53
  9. def OAI.KuroshConstruction.sequenceStage line 57
  10. def OAI.KuroshConstruction.sequenceStep line 60
  11. def OAI.KuroshConstruction.sequenceFieldMap line 65
  12. lemma OAI.KuroshConstruction.sequenceFieldMap_self line 69
  13. lemma OAI.KuroshConstruction.sequenceFieldMap_succ line 74
  14. lemma OAI.KuroshConstruction.sequenceFieldMap_trans line 80
  15. instance OAI.KuroshConstruction.sequenceDirectedSystem line 90
  16. lemma OAI.KuroshConstruction.sequence_task_new line 97
  17. lemma OAI.KuroshConstruction.sequence_task_old line 106
  18. lemma OAI.KuroshConstruction.sequence_task_transport line 112
  19. lemma OAI.KuroshConstruction.sequence_degree_growth line 123