OAI/Algebra/AffineCancellation/CylinderMaps.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ComplexCancellation.Cylinder.encode line 10
  2. def OAI.ComplexCancellation.Cylinder.decode line 14
  3. lemma OAI.ComplexCancellation.Cylinder.decode_equation line 17
  4. lemma OAI.ComplexCancellation.Cylinder.encode_decode line 22
  5. lemma OAI.ComplexCancellation.Cylinder.decode_encode line 27
  6. def OAI.ComplexCancellation.Cylinder.Point.map line 61
  7. lemma OAI.ComplexCancellation.Cylinder.Point.map_x line 64
  8. lemma OAI.ComplexCancellation.Cylinder.Point.map_equation line 67
  9. lemma OAI.ComplexCancellation.Cylinder.Point.map_shift line 71
  10. def OAI.ComplexCancellation.Cylinder.Frame.map line 78
  11. lemma OAI.ComplexCancellation.Cylinder.Frame.map_point line 80
  12. lemma OAI.ComplexCancellation.Cylinder.Frame.map_L line 84
  13. lemma OAI.ComplexCancellation.Cylinder.Frame.map_W line 88
  14. lemma OAI.ComplexCancellation.Cylinder.decode_map line 94
  15. lemma OAI.ComplexCancellation.Cylinder.encode_map line 98