OAI/MathematicalPhysics/NavierStokes/BalancedTransport/EffectiveArithmetic.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BalancedTransport.Effectivity.primrec_int_ofNat line 9
  2. lemma OAI.BalancedTransport.Effectivity.primrec_int_negSucc line 13
  3. lemma OAI.BalancedTransport.Effectivity.primrec_int_cases line 17
  4. lemma OAI.BalancedTransport.Effectivity.primrec_int_natAbs line 33
  5. lemma OAI.BalancedTransport.Effectivity.primrec_int_toNat line 37
  6. lemma OAI.BalancedTransport.Effectivity.primrec_int_neg line 41
  7. lemma OAI.BalancedTransport.Effectivity.primrec_int_natSub line 50
  8. lemma OAI.BalancedTransport.Effectivity.primrec_int_add line 60
  9. lemma OAI.BalancedTransport.Effectivity.primrec_int_mul line 75
  10. lemma OAI.BalancedTransport.Effectivity.computable_find line 91
  11. lemma OAI.BalancedTransport.Effectivity.primrec_nat_dvd line 103
  12. lemma OAI.BalancedTransport.Effectivity.primrec_nat_gcd line 107
  13. lemma OAI.BalancedTransport.Effectivity.primrec_nat_coprime line 128
  14. def OAI.BalancedTransport.Effectivity.rawRatCode line 132
  15. def OAI.BalancedTransport.Effectivity.validRatCode line 134
  16. instance OAI.BalancedTransport.Effectivity.(instance at line 137) line 137
  17. lemma OAI.BalancedTransport.Effectivity.primrec_validRatCode line 139
  18. lemma OAI.BalancedTransport.Effectivity.rawRatCode_eq line 145
  19. lemma OAI.BalancedTransport.Effectivity.validRatCode_iff line 147
  20. def OAI.BalancedTransport.Effectivity.ratRank line 159
  21. lemma OAI.BalancedTransport.Effectivity.primrec_ratRank line 161
  22. lemma OAI.BalancedTransport.Effectivity.ratRank_code line 164
  23. lemma OAI.BalancedTransport.Effectivity.rawRatCode_injective line 173
  24. lemma OAI.BalancedTransport.Effectivity.ratRank_injective_valid line 176
  25. lemma OAI.BalancedTransport.Effectivity.computable_rawRatCode line 184
  26. lemma OAI.BalancedTransport.Effectivity.computable_rat_num line 198
  27. lemma OAI.BalancedTransport.Effectivity.computable_rat_den line 204
  28. lemma OAI.BalancedTransport.Effectivity.rat_fraction_eq_iff line 208
  29. lemma OAI.BalancedTransport.Effectivity.computable_rat_of_parts line 215
  30. lemma OAI.BalancedTransport.Effectivity.computable_rat_add line 242
  31. lemma OAI.BalancedTransport.Effectivity.computable_rat_mul line 261
  32. lemma OAI.BalancedTransport.Effectivity.computable_rat_neg line 272