OAI/Analysis/JiangSu/DimensionDrop/ToeplitzDimensionDrop.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentMain.ProjectionRow.matrixHom_matrixUnit line 22
  2. def OAI.CurrentMain.ProjectionRow.toeplitzWitness line 28
  3. theorem OAI.CurrentMain.Traceless.empty_comparison_dimension_drop_hom line 71
  4. theorem OAI.CurrentMain.Traceless.empty_comparison_prime_drop_hom line 89
  5. theorem OAI.CurrentMain.Traceless.empty_comparison_original_jiang_su_embedding line 116
  6. theorem OAI.OriginalJiangSu.spatial_connected_half_flip line 149
  7. theorem OAI.OriginalJiangSu.spatial_half_flip line 153
  8. theorem OAI.OriginalJiangSu.absorption_of_embedding line 160
  9. theorem OAI.OriginalJiangSu.absorption_of_embedding_exists line 167
  10. theorem OAI.DirectComparison.comparison_original_jiang_su_absorption line 183
  11. theorem OAI.CurrentMain.Traceless.empty_comparison_original_jiang_su_absorption line 199
  12. theorem OAI.NonunitalSI.comparison_original_jiang_su_absorption line 216