OAI/GroupTheory/FiniteType/ActionTransport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ActionTransport.exists_liftedFrames line 23
2. def OAI.ActionTransport.edgeLeftHom line 55
3. def OAI.ActionTransport.edgeRightHom line 64
4. lemma OAI.ActionTransport.coherent_of_generators line 77
5. lemma OAI.ActionTransport.edge_defect_projects line 93
6. theorem OAI.ActionTransport.finite_flat_quotient line 105
7. theorem OAI.ActionTransport.finitelyPresented_of_frames line 183
8. def OAI.ActionTransport.orbitFrames line 214
9. lemma OAI.ActionTransport.finite_orbits_of_cover line 225
10. lemma OAI.ActionTransport.finite_orbits_of_map line 234