OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkActualUniversalPrincipalReplacement.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryBulkActualUniversalPrincipal.transportReference line 27
2. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualUniversalPrincipal.transportReference_frame line 42
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualUniversalPrincipal.transportReference_permutation line 50
4. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualUniversalPrincipal.transportReference_weight line 58
5. def OAI.Ostmann.Arithmetic.HistoryBulkActualUniversalPrincipal.replacementReference line 74
6. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualUniversalPrincipal.replacementReference_frame line 83
7. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualUniversalPrincipal.replacementReference_permutation line 88
8. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualUniversalPrincipal.replacementReference_term line 93