OAI/MathematicalPhysics/RapidForcing/RatPrimrec.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_nat_coprime line 11
2. lemma OAI.RapidForcing.EffectiveArithmetic.rat_encoding line 15
3. lemma OAI.RapidForcing.EffectiveArithmetic.rat_roundtrip line 17
4. instance OAI.RapidForcing.EffectiveArithmetic.ratPrimcodable line 30
5. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_rat_num line 41
6. lemma OAI.RapidForcing.EffectiveArithmetic.primrec_rat_den line 46