OAI/Analysis/MatrixSigning/Arithmetic/RationalAddModel.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W13.RationalAdd.signedNumerator line 14
2. theorem OAI.KS.W13.RationalAdd.signedNumerator_value line 20
3. theorem OAI.KS.W13.RationalAdd.subtractResult_length_le line 29
4. theorem OAI.KS.W13.RationalAdd.signedNumerator_length_le line 39
5. theorem OAI.KS.W13.RationalAdd.signedNumerator_canonical line 53
6. def OAI.KS.W13.RationalAdd.rawSum line 60
7. theorem OAI.KS.W13.RationalAdd.rawSum_value line 65
8. theorem OAI.KS.W13.RationalAdd.rawSum_encoded_value line 81