OAI/GroupTheory/FiniteType/SurjectiveTrivialInduction.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SurjectiveTrivialInduction.mk_eq line 19
  2. def OAI.SurjectiveTrivialInduction.forward line 26
  3. lemma OAI.SurjectiveTrivialInduction.forward_mk line 28
  4. def OAI.SurjectiveTrivialInduction.backward line 32
  5. def OAI.SurjectiveTrivialInduction.iso line 42
  6. theorem OAI.OrbitModule.trivial_presentation_of_fg line 67
  7. instance OAI.ProductGroupHomology.action line 82
  8. lemma OAI.ProductGroupHomology.action_def line 91
  9. instance OAI.ProductGroupHomology.(instance at line 93) line 93
  10. def OAI.ProductGroupHomology.stabilizerEquiv line 100
  11. def OAI.ProductGroupHomology.freePermIso line 112
  12. lemma OAI.ProductGroupHomology.free_coordinates line 134
  13. lemma OAI.ProductGroupHomology.free_acyclic line 144
  14. abbrev OAI.ProductGroupHomology.R line 159
  15. def OAI.ProductGroupHomology.C line 160
  16. def OAI.ProductGroupHomology.d line 163
  17. lemma OAI.ProductGroupHomology.w line 166
  18. instance OAI.ProductGroupHomology.(instance at line 174) line 174
  19. lemma OAI.ProductGroupHomology.exact line 176
  20. theorem OAI.ProductGroupHomology.products line 181
  21. lemma OAI.ActionPresentation.ker_retraction_fg line 215
  22. lemma OAI.ActionPresentation.finitelyPresented_retract line 247
  23. def OAI.ActionPresentation.descend line 257
  24. lemma OAI.ActionPresentation.descend_comp line 262
  25. structure OAI.ActionPresentation.LiftModel line 273
  26. def OAI.ActionPresentation.liftModel line 283
  27. def OAI.ActionPresentation.LiftModel.obstruction line 294
  28. lemma OAI.ActionPresentation.LiftModel.obstruction_finite line 295
  29. lemma OAI.ActionPresentation.LiftModel.obstruction_ker line 296
  30. lemma OAI.ActionPresentation.LiftModel.ker_le line 304
  31. def OAI.ActionPresentation.LiftModel.hom line 310
  32. lemma OAI.ActionPresentation.LiftModel.hom_comp line 312
  33. lemma OAI.ActionPresentation.LiftModel.hom_commutes line 314
  34. def OAI.ActionPresentation.killProjection line 325
  35. lemma OAI.ActionPresentation.killProjection_comp line 328
  36. lemma OAI.ActionPresentation.killProjection_surj line 330
  37. lemma OAI.ActionPresentation.kill_finitelyPresented line 335
  38. lemma OAI.ActionPresentation.fg_of_fp line 343
  39. lemma OAI.ActionPresentation.commute_of_generators line 347
  40. lemma OAI.ActionPresentation.product_finitelyPresented line 365
  41. lemma OAI.ActionPresentation.finite_pi_finitelyPresented line 410