OAI/GroupTheory/PolycyclicRecognition/Algebra/RepresentationDirectSum.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Concrete sums of integral representations for the telescope resolution

  1. abbrev OAI.PolycyclicRecognition.integralRepresentationSum line 13
  2. abbrev OAI.PolycyclicRecognition.integralRepresentationSumInclusion line 16
  3. theorem OAI.PolycyclicRecognition.integralRepresentationSumInclusion_apply line 24
  4. theorem OAI.PolycyclicRecognition.integralRepresentationSumInclusion_same line 32
  5. theorem OAI.PolycyclicRecognition.integralRepresentationSumInclusion_ne line 39
  6. def OAI.PolycyclicRecognition.integralRepresentationSumDesc line 46
  7. theorem OAI.PolycyclicRecognition.integralRepresentationSumInclusion_desc line 61
  8. theorem OAI.PolycyclicRecognition.integralRepresentationSum_hom_ext line 74
  9. instance OAI.PolycyclicRecognition.integralRepresentationSum_projective line 85