OAI/NumberTheory/Ostmann/Construction/CanonicalEnumeration.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Ostmann.Construction.assignedSlots_injective line 9
  2. def OAI.Ostmann.Construction.History.nodeCompensation line 19
  3. def OAI.Ostmann.Construction.History.nodeLeft line 22
  4. def OAI.Ostmann.Construction.History.nodeRight line 25
  5. theorem OAI.Ostmann.Construction.decodeHistory_injective line 30
  6. def OAI.Ostmann.Construction.canonicalHistoryPool line 67
  7. theorem OAI.Ostmann.Construction.canonicalCoefficient_eq_coefficient line 72