OAI/MathematicalPhysics/RapidForcing/RatComputable.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RapidForcing.EffectiveArithmetic.computable_of_graph line 9
2. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_rat_le line 34
3. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_rat_lt line 38
4. lemma OAI.RapidForcing.EffectiveArithmetic.rat_div_graph line 42
5. lemma OAI.RapidForcing.EffectiveArithmetic.computable_rat_divNat line 49
6. lemma OAI.RapidForcing.EffectiveArithmetic.computable_rat_castInt line 60
7. lemma OAI.RapidForcing.EffectiveArithmetic.computable_rat_castNat line 63
8. lemma OAI.RapidForcing.EffectiveArithmetic.computable_rat_add line 66
9. lemma OAI.RapidForcing.EffectiveArithmetic.computable_rat_mul line 77
10. lemma OAI.RapidForcing.EffectiveArithmetic.computable_rat_neg line 84
11. lemma OAI.RapidForcing.EffectiveArithmetic.computable_rat_sub line 90