OAI/Topology/ArtinGroups/Cancellation/Remainder.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicArtin.GaussianCancellation.remainder line 10
  2. theorem OAI.HarmonicArtin.GaussianCancellation.remainder_commutes line 12
  3. theorem OAI.HarmonicArtin.GaussianCancellation.h_mul_remainder line 18
  4. theorem OAI.HarmonicArtin.GaussianCancellation.remainder_mul_h line 23
  5. theorem OAI.HarmonicArtin.GaussianCancellation.remainder_idempotent line 29
  6. theorem OAI.HarmonicArtin.GaussianCancellation.remainder_homotopy line 42
  7. def OAI.HarmonicArtin.GaussianCancellation.pivotHomotopy line 54
  8. theorem OAI.HarmonicArtin.GaussianCancellation.pivotHomotopy_square line 57
  9. theorem OAI.HarmonicArtin.GaussianCancellation.pivotHomotopy_retract line 66
  10. abbrev OAI.HarmonicArtin.GaussianCancellation.Reduced line 77
  11. def OAI.HarmonicArtin.GaussianCancellation.reducedDifferential line 82
  12. theorem OAI.HarmonicArtin.GaussianCancellation.reducedDifferential_square line 88
  13. def OAI.HarmonicArtin.GaussianCancellation.projectReduced line 95
  14. theorem OAI.HarmonicArtin.GaussianCancellation.projection_inclusion line 97
  15. theorem OAI.HarmonicArtin.GaussianCancellation.inclusion_projection line 105
  16. theorem OAI.HarmonicArtin.GaussianCancellation.inclusion_chainMap line 108
  17. theorem OAI.HarmonicArtin.GaussianCancellation.projection_chainMap line 112