OAI/Analysis/MatrixSigning/Arithmetic/RationalCompareDeterministic.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.KS.W06.RationalCompareDeterministic.sign_coinIndependent line 14
  2. theorem OAI.KS.W06.RationalCompareDeterministic.decode_coinIndependent line 19
  3. theorem OAI.KS.W06.RationalCompareDeterministic.liftedEntry_coinIndependent line 23
  4. theorem OAI.KS.W06.RationalCompareDeterministic.magnitudeCarry_coinIndependent line 30
  5. theorem OAI.KS.W06.RationalCompareDeterministic.magnitude_coinIndependent line 39
  6. theorem OAI.KS.W06.RationalCompareDeterministic.parse_coinIndependent line 44
  7. theorem OAI.KS.W06.RationalCompareDeterministic.prepare_coinIndependent line 57
  8. theorem OAI.KS.W06.RationalCompareDeterministic.product_coinIndependent line 62
  9. theorem OAI.KS.W06.RationalCompareDeterministic.products_coinIndependent line 66
  10. theorem OAI.KS.W06.RationalCompareDeterministic.compare_coinIndependent line 70
  11. theorem OAI.KS.W06.RationalCompareDeterministic.signedCompare_coinIndependent line 76
  12. theorem OAI.KS.W06.RationalCompareDeterministic.coinIndependent line 81
  13. theorem OAI.KS.W06.RationalCompareDeterministic.singleBase_coinIndependent line 86
  14. theorem OAI.KS.W06.RationalCompareDeterministic.singlePorts_coinIndependent line 95
  15. theorem OAI.KS.W06.RationalCompareDeterministic.single_coinIndependent line 99
  16. theorem OAI.KS.W06.RationalCompareDeterministic.canonicalPair_coinIndependent line 102