OAI/Analysis/MatrixSigning/Arithmetic/RationalReciprocalSwap.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W30.RationalReciprocal.transfer line 10
  2. def OAI.KS.W30.RationalReciprocal.transferred line 14
  3. theorem OAI.KS.W30.RationalReciprocal.transfer_spec line 17
  4. def OAI.KS.W30.RationalReciprocal.saveNumerator line 61
  5. def OAI.KS.W30.RationalReciprocal.shiftDenominator line 62
  6. def OAI.KS.W30.RationalReciprocal.restoreNumerator line 63
  7. def OAI.KS.W30.RationalReciprocal.swap line 64
  8. def OAI.KS.W30.RationalReciprocal.savedState line 66
  9. def OAI.KS.W30.RationalReciprocal.shiftedState line 68
  10. theorem OAI.KS.W30.RationalReciprocal.saveNumerator_spec line 71
  11. theorem OAI.KS.W30.RationalReciprocal.shiftDenominator_spec line 80
  12. theorem OAI.KS.W30.RationalReciprocal.restoreNumerator_spec line 88
  13. theorem OAI.KS.W30.RationalReciprocal.swap_spec line 97