OAI/MathematicalPhysics/RapidForcing/ArithmeticAutomation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_int_cast line 19
  2. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_nat_add line 21
  3. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_nat_sub line 22
  4. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_nat_mul line 23
  5. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_nat_div line 24
  6. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_nat_mod line 25
  7. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_nat_max line 26
  8. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_nat_min line 27
  9. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_nat_le line 28
  10. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_nat_lt line 29
  11. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_eq line 30
  12. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_nat_pow line 33
  13. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_factorial line 43
  14. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_int_subNat line 51
  15. lemma OAI.RapidForcing.EffectiveArithmetic.int_difference_parts line 57
  16. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_int_add line 59
  17. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_int_sub line 66
  18. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_int_mul line 69
  19. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_int_le line 79
  20. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_int_lt line 84
  21. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_nat_gcd line 88