OAI/Analysis/MatrixSigning/Arithmetic/BinaryRationalAdd.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W30.BinaryRational.signedValue line 11
2. def OAI.KS.W30.BinaryRational.addSigned line 14
3. theorem OAI.KS.W30.BinaryRational.addSigned_value line 20
4. theorem OAI.KS.W30.BinaryRational.addSigned_length line 47
5. def OAI.KS.W30.BinaryRational.addSignedWork line 60
6. theorem OAI.KS.W30.BinaryRational.addSignedWork_linear line 66
7. def OAI.KS.W30.BinaryRational.addRat line 75
8. lemma OAI.KS.W30.BinaryRational.value_eq_signed_div line 80
9. lemma OAI.KS.W30.BinaryRational.signedValue_multiply line 84
10. theorem OAI.KS.W30.BinaryRational.addRat_value line 88
11. def OAI.KS.W30.BinaryRational.addRatWork line 99
12. theorem OAI.KS.W30.BinaryRational.addRatWork_polynomial line 107