OAI/Computability/DegreeRigidity/CohenForcing/CohenProductSplitting.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TuringRigidity.CohenProductSplitting.productMapline 10 - theorem
OAI.TuringRigidity.CohenProductSplitting.label_productMapline 16 - def
OAI.TuringRigidity.CohenProductSplitting.productIsoline 22 - def
OAI.TuringRigidity.CohenProductSplitting.putBitline 41 - theorem
OAI.TuringRigidity.CohenProductSplitting.putBit_leline 46 - theorem
OAI.TuringRigidity.CohenProductSplitting.putBit_incompatibleline 54 - theorem
OAI.TuringRigidity.CohenProductSplitting.cohen_splitsline 63 - theorem
OAI.TuringRigidity.CohenProductSplitting.product_splitsline 90