OAI/Computability/DegreeRigidity/OrdinalCodes/OrdinalSumClosure.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TuringRigidity.OrdinalArithmetic.ordinal_add_internal_schemas line 9
2. theorem OAI.TuringRigidity.OrdinalArithmetic.ordinal_mul_nat_internal_schemas line 23
3. theorem OAI.TuringRigidity.OrdinalArithmetic.ordinal_mul_two_internal line 33
4. def OAI.TuringRigidity.OrdinalArithmetic.doubleSentence line 38
5. theorem OAI.TuringRigidity.OrdinalArithmetic.doubleSentence_bound line 41
6. theorem OAI.TuringRigidity.OrdinalArithmetic.doubleSentence_sound line 43
7. theorem OAI.TuringRigidity.OrdinalArithmetic.doubleSentence_sourceT line 49