OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairRepresentatives.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryPairRepresentatives.internalSlot_prime line 12
2. theorem OAI.Ostmann.Arithmetic.HistoryPairRepresentatives.slot_prime line 28
3. def OAI.Ostmann.Arithmetic.HistoryPairRepresentatives.key line 34
4. def OAI.Ostmann.Arithmetic.HistoryPairRepresentatives.Representative line 36
5. instance OAI.Ostmann.Arithmetic.HistoryPairRepresentatives.(instance at line 38) line 38
6. instance OAI.Ostmann.Arithmetic.HistoryPairRepresentatives.(instance at line 41) line 41
7. def OAI.Ostmann.Arithmetic.HistoryPairRepresentatives.label line 44
8. def OAI.Ostmann.Arithmetic.HistoryPairRepresentatives.prime line 47
9. def OAI.Ostmann.Arithmetic.HistoryPairRepresentatives.Fiber line 49
10. instance OAI.Ostmann.Arithmetic.HistoryPairRepresentatives.fiberFintype line 51
11. theorem OAI.Ostmann.Arithmetic.HistoryPairRepresentatives.label_surjective line 55
12. theorem OAI.Ostmann.Arithmetic.HistoryPairRepresentatives.label_eq_iff line 60
13. theorem OAI.Ostmann.Arithmetic.HistoryPairRepresentatives.prime_label line 69
14. theorem OAI.Ostmann.Arithmetic.HistoryPairRepresentatives.representative_prime line 72
15. theorem OAI.Ostmann.Arithmetic.HistoryPairRepresentatives.fiber_nonempty line 77
16. theorem OAI.Ostmann.Arithmetic.HistoryPairRepresentatives.product_occurrences line 81
17. theorem OAI.Ostmann.Arithmetic.HistoryPairRepresentatives.product_by_multiplicity line 86