OAI/Analysis/MatrixSigning/Arithmetic/RationalMultiplyNormalize.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W15.RationalMultiply.rawProduct line 14
2. theorem OAI.KS.W15.RationalMultiply.rawProduct_value line 18
3. def OAI.KS.W15.RationalMultiply.rawCanonicalProduct line 27
4. theorem OAI.KS.W15.RationalMultiply.rawCanonicalProduct_value line 32
5. def OAI.KS.W15.RationalMultiply.normalizeProgram line 40
6. def OAI.KS.W15.RationalMultiply.payloadSize line 44
7. def OAI.KS.W15.RationalMultiply.normalizeTicks line 46
8. theorem OAI.KS.W15.RationalMultiply.normalized_spec line 53
9. def OAI.KS.W15.RationalMultiply.canonicalNormalizeTicks line 80
10. theorem OAI.KS.W15.RationalMultiply.canonical_normalized_spec line 84
11. theorem OAI.KS.W15.RationalMultiply.cleanupTicks_le line 101
12. theorem OAI.KS.W15.RationalMultiply.normalizeTicks_le line 109
13. theorem OAI.KS.W15.RationalMultiply.canonicalNormalizeTicks_le line 143