OAI/Analysis/MatrixSigning/Arithmetic/RationalMultiplyProducts.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W15.RationalMultiply.numeratorPorts line 12
2. def OAI.KS.W15.RationalMultiply.denominatorPorts line 13
3. def OAI.KS.W15.RationalMultiply.productsProgram line 15
4. def OAI.KS.W15.RationalMultiply.productsAfter line 19
5. theorem OAI.KS.W15.RationalMultiply.products_spec line 24
6. def OAI.KS.W15.RationalMultiply.xorDispatch line 53
7. def OAI.KS.W15.RationalMultiply.xorProgram line 57
8. def OAI.KS.W15.RationalMultiply.xorAfter line 59
9. theorem OAI.KS.W15.RationalMultiply.xor_spec line 62
10. def OAI.KS.W15.RationalMultiply.cleanupProgram line 81
11. def OAI.KS.W15.RationalMultiply.cleanupTicks line 89
12. theorem OAI.KS.W15.RationalMultiply.cleanup_spec line 94