OAI/Algebra/Finitistic/Selected/SelectedPDDetection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.LittleFinitistic.SelectedPDDetection.residueModuleK line 14
2. instance OAI.LittleFinitistic.SelectedPDDetection.residueTowerK line 15
3. abbrev OAI.LittleFinitistic.SelectedPDDetection.barTensor line 19
4. def OAI.LittleFinitistic.SelectedPDDetection.torIsoBar line 23
5. theorem OAI.LittleFinitistic.SelectedPDDetection.pdLE_iff_residue_bar line 28
6. theorem OAI.LittleFinitistic.SelectedPDDetection.pdLE_iff_simple_bar line 33
7. theorem OAI.LittleFinitistic.SelectedPDDetection.finite_pd_of_bar line 39
8. theorem OAI.LittleFinitistic.SelectedPDDetection.lower_bound_of_bar line 45
9. theorem OAI.LittleFinitistic.SelectedPDDetection.finite_pd_of_derived_bar line 55
10. theorem OAI.LittleFinitistic.SelectedPDDetection.lower_bound_of_derived_bar line 63