OAI/NumberTheory/Ostmann/Arithmetic/HistoryOccurrenceVariables.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryOccurrenceVariables.InternalKey line 9
2. instance OAI.Ostmann.Arithmetic.HistoryOccurrenceVariables.internalKeyFintype line 14
3. def OAI.Ostmann.Arithmetic.HistoryOccurrenceVariables.internalSlot line 21
4. def OAI.Ostmann.Arithmetic.HistoryOccurrenceVariables.Key line 26
5. instance OAI.Ostmann.Arithmetic.HistoryOccurrenceVariables.keyFintype line 29
6. def OAI.Ostmann.Arithmetic.HistoryOccurrenceVariables.integerSample line 32
7. def OAI.Ostmann.Arithmetic.HistoryOccurrenceVariables.rationalSample line 38
8. theorem OAI.Ostmann.Arithmetic.HistoryOccurrenceVariables.internalKey_card line 40
9. theorem OAI.Ostmann.Arithmetic.HistoryOccurrenceVariables.key_card line 49
10. theorem OAI.Ostmann.Arithmetic.HistoryOccurrenceVariables.prod_internalSlot line 54