OAI/GroupTheory/PolycyclicRecognition/Analysis/IntegralQuotientKernel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Removing one coordinate from an integral abelian quotient

  1. def OAI.PolycyclicRecognition.integralQuotientDrop line 11
  2. def OAI.PolycyclicRecognition.integralQuotientLast line 16
  3. def OAI.PolycyclicRecognition.integralQuotientInsert line 21
  4. theorem OAI.PolycyclicRecognition.integralQuotientDrop_insert line 24
  5. theorem OAI.PolycyclicRecognition.integralQuotientLast_insert line 31
  6. theorem OAI.PolycyclicRecognition.integralQuotientLast_surjective line 37
  7. theorem OAI.PolycyclicRecognition.integralQuotient_eq_one line 40
  8. def OAI.PolycyclicRecognition.integralLastMap line 50
  9. def OAI.PolycyclicRecognition.integralKernelInl line 53
  10. def OAI.PolycyclicRecognition.integralKernelRight line 59
  11. def OAI.PolycyclicRecognition.integralKernelExtension line 63
  12. theorem OAI.PolycyclicRecognition.integralKernelExtension_conjAct line 93