OAI/Analysis/MatrixSigning/Arithmetic/BinaryRationalCore.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.KS.W30.BinaryRational.RatBits line 12
2. def OAI.KS.W30.BinaryRational.RatBits.length line 18
3. def OAI.KS.W30.BinaryRational.RatBits.magnitude line 20
4. def OAI.KS.W30.BinaryRational.RatBits.value line 23
5. def OAI.KS.W30.BinaryRational.normalize line 25
6. lemma OAI.KS.W30.BinaryRational.normalizeMagnitude_value line 29
7. theorem OAI.KS.W30.BinaryRational.normalize_value line 48
8. def OAI.KS.W30.BinaryRational.encodeMagnitude line 61
9. def OAI.KS.W30.BinaryRational.multiplyRat line 65
10. def OAI.KS.W30.BinaryRational.inverseRat line 69
11. theorem OAI.KS.W30.BinaryRational.multiplyRat_value line 72
12. theorem OAI.KS.W30.BinaryRational.inverseRat_value line 78
13. def OAI.KS.W30.BinaryRational.multiplyRatWork line 82
14. def OAI.KS.W30.BinaryRational.inverseRatWork line 87
15. theorem OAI.KS.W30.BinaryRational.multiplyRatWork_polynomial line 90
16. theorem OAI.KS.W30.BinaryRational.inverseRatWork_polynomial line 112