OAI/Analysis/MatrixSigning/Arithmetic/RationalArithmeticMeter.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.KS.W17.RationalExpr line 10
  2. def OAI.KS.W17.RationalExpr.eval line 18
  3. def OAI.KS.W17.RationalExpr.operations line 26
  4. def OAI.KS.W17.sumExpr line 31
  5. theorem OAI.KS.W17.sumExpr_eval line 35
  6. theorem OAI.KS.W17.sumExpr_operations line 41
  7. def OAI.KS.W17.dotExpr line 47
  8. theorem OAI.KS.W17.dotExpr_eval line 50
  9. theorem OAI.KS.W17.dotExpr_operations line 54
  10. def OAI.KS.W17.schurEntryExpr line 58
  11. theorem OAI.KS.W17.schurEntryExpr_eval line 63
  12. theorem OAI.KS.W17.schurEntryExpr_operations line 67
  13. def OAI.KS.W17.liftHeadExpr line 71
  14. theorem OAI.KS.W17.liftHeadExpr_eval line 75
  15. theorem OAI.KS.W17.liftHeadExpr_operations line 80
  16. def OAI.KS.W17.zeroPivotExpr line 85
  17. theorem OAI.KS.W17.zeroPivotExpr_eval line 88
  18. theorem OAI.KS.W17.zeroPivotExpr_operations line 91