OAI/NumberTheory/Ostmann/Characters/TemplateHistory.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Ostmann.Characters.Template.State line 11
  2. def OAI.Ostmann.Characters.Template.copiedProduct line 13
  3. def OAI.Ostmann.Characters.Template.reconstructedPivot line 16
  4. def OAI.Ostmann.Characters.Template.childState line 19
  5. theorem OAI.Ostmann.Characters.Template.childState_pivot line 24
  6. theorem OAI.Ostmann.Characters.Template.childState_copied line 28
  7. theorem OAI.Ostmann.Characters.Template.childState_outside line 35
  8. structure OAI.Ostmann.Characters.Template.NodeSupported line 40
  9. theorem OAI.Ostmann.Characters.Template.NodeSupported.unique line 52
  10. def OAI.Ostmann.Characters.Template.Supported line 63
  11. theorem OAI.Ostmann.Characters.Template.supported_unique line 73
  12. def OAI.Ostmann.Characters.Template.leafStates line 92
  13. theorem OAI.Ostmann.Characters.Template.leafStates_length line 101