OAI/GroupTheory/PolycyclicRecognition/Algebra/NormalizedFreeColimit.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Normalized free generators in a sequential coefficient colimit

  1. abbrev OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeDiagram line 16
  2. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeLimitGenerator line 18
  3. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeLimitGenerator_transport line 23
  4. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeLimitGenerator_zero line 41
  5. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeLimitGenerator_eq line 45
  6. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeLimitGenerator_eq_zero line 66
  7. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.normalizedFreeModuleBasis line 71
  8. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeModuleGenerator line 75
  9. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeModuleGenerator_zero line 79
  10. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeModuleGenerator_basis line 82
  11. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeModuleCocone line 88
  12. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeModuleLift line 92
  13. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeModuleLift_generator line 101
  14. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeChosenLift line 108
  15. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeModuleInverse line 112
  16. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeModuleInverse_basis line 117
  17. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeLimitGenerator_basis line 122
  18. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeModuleLift_chosen line 130
  19. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeModuleInverse_generator line 135
  20. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeModuleLift_bijective line 146
  21. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.freeModuleLift_of line 170
  22. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.ColimitCocone.normalizedFree line 174