OAI/MathematicalPhysics/AlternatingFlow/Arithmetic.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AlternatingNS.Arithmetic.int_natCast line 10
  2. lemma OAI.AlternatingNS.Arithmetic.int_negSucc line 14
  3. lemma OAI.AlternatingNS.Arithmetic.int_cases line 18
  4. lemma OAI.AlternatingNS.Arithmetic.int_toNat line 36
  5. lemma OAI.AlternatingNS.Arithmetic.int_abs line 41
  6. lemma OAI.AlternatingNS.Arithmetic.int_diff line 46
  7. lemma OAI.AlternatingNS.Arithmetic.int_neg line 55
  8. lemma OAI.AlternatingNS.Arithmetic.int_add line 66
  9. lemma OAI.AlternatingNS.Arithmetic.int_sub line 73
  10. lemma OAI.AlternatingNS.Arithmetic.int_mul line 76
  11. lemma OAI.AlternatingNS.Arithmetic.nat_dvd line 108
  12. lemma OAI.AlternatingNS.Arithmetic.nat_gcd line 112
  13. lemma OAI.AlternatingNS.Arithmetic.rat_valid line 131
  14. def OAI.AlternatingNS.Arithmetic.ratEquiv line 135
  15. def OAI.AlternatingNS.Arithmetic.rationalCoding line 141
  16. lemma OAI.AlternatingNS.Arithmetic.rationalCoding_encode line 145
  17. lemma OAI.AlternatingNS.Arithmetic.rat_num line 150
  18. lemma OAI.AlternatingNS.Arithmetic.rat_den line 155
  19. lemma OAI.AlternatingNS.Arithmetic.int_ediv_nat line 160
  20. lemma OAI.AlternatingNS.Arithmetic.rat_mk line 173
  21. lemma OAI.AlternatingNS.Arithmetic.rat_intCast line 188
  22. lemma OAI.AlternatingNS.Arithmetic.rat_natCast line 191
  23. lemma OAI.AlternatingNS.Arithmetic.rat_add line 194
  24. lemma OAI.AlternatingNS.Arithmetic.rat_mul line 203
  25. lemma OAI.AlternatingNS.Arithmetic.rat_neg line 208
  26. lemma OAI.AlternatingNS.Arithmetic.rat_sub line 213
  27. lemma OAI.AlternatingNS.Arithmetic.int_le line 216
  28. lemma OAI.AlternatingNS.Arithmetic.int_lt line 220
  29. lemma OAI.AlternatingNS.Arithmetic.rat_divInt line 223
  30. lemma OAI.AlternatingNS.Arithmetic.rat_inv line 233
  31. lemma OAI.AlternatingNS.Arithmetic.rat_div line 236
  32. lemma OAI.AlternatingNS.Arithmetic.rat_le line 240
  33. lemma OAI.AlternatingNS.Arithmetic.rat_lt line 246
  34. lemma OAI.AlternatingNS.Arithmetic.rat_abs line 249
  35. lemma OAI.AlternatingNS.Arithmetic.rat_floor line 257
  36. lemma OAI.AlternatingNS.Arithmetic.rat_pow line 261