OAI/Analysis/FreeWords/ConcreteCornerAlgebra.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.KKConcreteCorner.extend_mul_compress line 20
  2. theorem OAI.KKConcreteCorner.extend_compress_mul line 28
  3. def OAI.KKConcreteCorner.centralizerVNA line 34
  4. def OAI.KKConcreteCorner.cornerAlgebra line 40
  5. theorem OAI.KKConcreteCorner.mem_cornerAlgebra_iff line 43
  6. def OAI.KKConcreteCorner.liftLinear line 68
  7. theorem OAI.KKConcreteCorner.lift_val line 74
  8. theorem OAI.KKConcreteCorner.lift_injective line 78
  9. theorem OAI.KKConcreteCorner.lift_mul line 84
  10. theorem OAI.KKConcreteCorner.lift_star line 89
  11. def OAI.KKConcreteCorner.restrict line 94
  12. theorem OAI.KKConcreteCorner.restrict_lift line 100
  13. def OAI.KKConcreteCorner.projection line 120
  14. theorem OAI.KKConcreteCorner.lift_one line 122
  15. theorem OAI.KKConcreteCorner.projection_isStar' line 124
  16. theorem OAI.KKConcreteCorner.lift_restrict line 129
  17. theorem OAI.KKConcreteCorner.lift_supported line 133
  18. theorem OAI.KKConcreteCorner.lift_projection line 138