OAI/NumberTheory/Ostmann/Construction/CanonicalHistoryProductChoicesDefs.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Construction.FrequencyChoices line 9
  2. instance OAI.Ostmann.Construction.frequencyChoicesFintype line 14
  3. abbrev OAI.Ostmann.Construction.InternalSourceDraws line 21
  4. instance OAI.Ostmann.Construction.internalSourceDrawsFintype line 24
  5. def OAI.Ostmann.Construction.internalSourcePrior line 30
  6. def OAI.Ostmann.Construction.historyFrequencies line 35
  7. def OAI.Ostmann.Construction.historyDraws line 42
  8. def OAI.Ostmann.Construction.assembleHistoryChoices line 49