OAI/Analysis/MatrixSigning/Arithmetic/RationalArithmetic.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W01.RationalComplex.zero line 12
  2. def OAI.KS.W01.RationalComplex.one line 13
  3. def OAI.KS.W01.RationalComplex.add line 14
  4. def OAI.KS.W01.RationalComplex.neg line 15
  5. def OAI.KS.W01.RationalComplex.mul line 16
  6. def OAI.KS.W01.RationalComplex.conj line 18
  7. def OAI.KS.W01.RationalComplex.normSq line 19
  8. def OAI.KS.W01.RationalComplex.inv line 20
  9. theorem OAI.KS.W01.RationalComplex.toComplex_zero line 23
  10. theorem OAI.KS.W01.RationalComplex.toComplex_one line 26
  11. theorem OAI.KS.W01.RationalComplex.toComplex_add line 29
  12. theorem OAI.KS.W01.RationalComplex.toComplex_neg line 33
  13. theorem OAI.KS.W01.RationalComplex.toComplex_mul line 37
  14. theorem OAI.KS.W01.RationalComplex.toComplex_conj line 41
  15. theorem OAI.KS.W01.RationalComplex.toReal_normSq line 45
  16. theorem OAI.KS.W01.RationalComplex.toComplex_inv line 49