OAI/MathematicalPhysics/SheetFlows/Computing.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

SheetFlows computing.

  1. theorem OAI.Solenoidal.Computing.gcd_findGreatest line 12
  2. theorem OAI.Solenoidal.Computing.nat_dvd line 32
  3. theorem OAI.Solenoidal.Computing.nat_gcd line 36
  4. theorem OAI.Solenoidal.Computing.encode_int_ofNat line 43
  5. theorem OAI.Solenoidal.Computing.encode_int_negSucc line 44
  6. theorem OAI.Solenoidal.Computing.int_ofNat line 46
  7. theorem OAI.Solenoidal.Computing.int_negSucc line 49
  8. def OAI.Solenoidal.Computing.intToSum line 52
  9. theorem OAI.Solenoidal.Computing.intToSum_pr line 54
  10. theorem OAI.Solenoidal.Computing.int_cases line 57
  11. theorem OAI.Solenoidal.Computing.int_natAbs line 63
  12. theorem OAI.Solenoidal.Computing.int_neg line 67
  13. theorem OAI.Solenoidal.Computing.int_subNatNat line 77
  14. theorem OAI.Solenoidal.Computing.int_add line 88
  15. theorem OAI.Solenoidal.Computing.int_mul line 105
  16. theorem OAI.Solenoidal.Computing.int_edivNat line 124
  17. theorem OAI.Solenoidal.Computing.int_nonneg line 136
  18. theorem OAI.Solenoidal.Computing.int_le line 144
  19. theorem OAI.Solenoidal.Computing.int_lt line 148
  20. def OAI.Solenoidal.Computing.ratValid line 151
  21. instance OAI.Solenoidal.Computing.(instance at line 153) line 153
  22. theorem OAI.Solenoidal.Computing.ratValid_pr line 156
  23. instance OAI.Solenoidal.Computing.ratPairPrimcodable line 161
  24. def OAI.Solenoidal.Computing.ratEquiv line 164
  25. instance OAI.Solenoidal.Computing.ratPrimcodable line 170
  26. theorem OAI.Solenoidal.Computing.rat_encoding line 172
  27. theorem OAI.Solenoidal.Computing.rat_num line 175
  28. theorem OAI.Solenoidal.Computing.rat_den line 178
  29. theorem OAI.Solenoidal.Computing.rat_mk_iff line 181
  30. theorem OAI.Solenoidal.Computing.rat_mk line 187
  31. theorem OAI.Solenoidal.Computing.rat_int line 197
  32. theorem OAI.Solenoidal.Computing.rat_nat line 200
  33. theorem OAI.Solenoidal.Computing.rat_neg line 202
  34. theorem OAI.Solenoidal.Computing.rat_add line 205
  35. theorem OAI.Solenoidal.Computing.rat_sub line 212
  36. theorem OAI.Solenoidal.Computing.rat_mul line 215
  37. theorem OAI.Solenoidal.Computing.rat_le line 221
  38. theorem OAI.Solenoidal.Computing.rat_lt line 227
  39. theorem OAI.Solenoidal.Computing.rat_abs line 230
  40. theorem OAI.Solenoidal.Computing.rat_inv line 236
  41. theorem OAI.Solenoidal.Computing.rat_div line 250
  42. theorem OAI.Solenoidal.Computing.rat_max line 253
  43. theorem OAI.Solenoidal.Computing.rat_pow line 256
  44. theorem OAI.Solenoidal.Computing.nat_factorial line 263
  45. theorem OAI.Solenoidal.Computing.rat_floor line 271
  46. theorem OAI.Solenoidal.Computing.ball_point line 284
  47. theorem OAI.Solenoidal.Computing.ball_add line 285
  48. theorem OAI.Solenoidal.Computing.ball_neg line 288
  49. theorem OAI.Solenoidal.Computing.ball_mul line 290
  50. theorem OAI.Solenoidal.Computing.ball_pow line 297
  51. theorem OAI.Solenoidal.Computing.rat_sum_range line 304
  52. theorem OAI.Solenoidal.Computing.ball_taylor line 313
  53. theorem OAI.Solenoidal.Computing.ball_smallExp line 316
  54. theorem OAI.Solenoidal.Computing.ball_expScale line 320
  55. theorem OAI.Solenoidal.Computing.ball_expApprox line 323
  56. theorem OAI.Solenoidal.Computing.ball_clampInv line 328
  57. theorem OAI.Solenoidal.Computing.ball_flatApprox line 332
  58. theorem OAI.Solenoidal.Computing.ball_reciprocalApprox line 338