OAI/Computability/DegreeRigidity/OrdinalCodes/OrdinalProductClosure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TuringRigidity.OrdinalArithmetic.toZFSet_nat line 10
2. theorem OAI.TuringRigidity.OrdinalArithmetic.toZFSet_omega line 15
3. theorem OAI.TuringRigidity.OrdinalArithmetic.ordinal_mul_internal_schemas line 25
4. theorem OAI.TuringRigidity.OrdinalArithmetic.ordinal_mul_omega_internal line 39
5. theorem OAI.TuringRigidity.OrdinalArithmetic.ordinal_opow_nat_internal line 46