OAI/Analysis/JiangSu/CStarAlgebras/FourEdgeGroupSurgery.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.FourEdgeSurgery.Flow.map_zero line 11
  2. lemma OAI.FourEdgeSurgery.Flow.map_neg line 13
  3. lemma OAI.FourEdgeSurgery.Flow.commute line 16
  4. def OAI.FourEdgeSurgery.correction line 22
  5. def OAI.FourEdgeSurgery.surgery line 25
  6. lemma OAI.FourEdgeSurgery.correction_zero line 28
  7. lemma OAI.FourEdgeSurgery.correction_scalar_zero line 30
  8. lemma OAI.FourEdgeSurgery.correction_one line 32
  9. lemma OAI.FourEdgeSurgery.surgery_left_zero line 39
  10. lemma OAI.FourEdgeSurgery.surgery_left_one line 45
  11. lemma OAI.FourEdgeSurgery.surgery_right_zero line 52
  12. lemma OAI.FourEdgeSurgery.surgery_right_one line 66
  13. lemma OAI.FourEdgeSurgery.surgery_trivial line 81
  14. lemma OAI.FourEdgeSurgery.correction_continuous line 99
  15. lemma OAI.FourEdgeSurgery.surgery_continuous line 104