OAI/Analysis/JiangSu/Main.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OriginalJiangSu.Main.UnitalSpatialEquiv line 29
  2. theorem OAI.OriginalJiangSu.Main.nonunitalSpatial_addMemClass line 54
  3. theorem OAI.OriginalJiangSu.Main.nonunitalSpatial_mulMemClass line 61
  4. theorem OAI.OriginalJiangSu.Main.nonunitalSpatial_smulMemClass line 68
  5. theorem OAI.OriginalJiangSu.Main.nonunitalSpatial_starMemClass line 75
  6. abbrev OAI.OriginalJiangSu.Main.SpatialIdealEquiv line 82
  7. abbrev OAI.OriginalJiangSu.Main.NonunitalSpatialEquivCore line 96
  8. theorem OAI.OriginalJiangSu.Main.unitalSpatialEquiv_of_nonempty line 101
  9. theorem OAI.OriginalJiangSu.Main.unital_main line 107
  10. theorem OAI.OriginalJiangSu.Main.nonunitalSpatialEquiv_of_nonempty line 133
  11. theorem OAI.OriginalJiangSu.Main.stably_projectionless_main line 140