OAI/Analysis/FreeWords/CornerCentralScalar.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.KKConcreteCorner.closure_convexHull_subset_zero line 25
  2. def OAI.KKConcreteCorner.cornerOperator line 32
  3. theorem OAI.KKConcreteCorner.cornerOperator_orbit line 37
  4. theorem OAI.KKConcreteCorner.cornerOperator_hull line 49
  5. theorem OAI.KKConcreteCorner.cornerOperator_trace_zero line 56
  6. theorem OAI.KKConcreteCorner.gnsStarAlgHom_smul_one line 64
  7. theorem OAI.KKConcreteCorner.cornerOperator_trace_value line 69
  8. theorem OAI.KKConcreteCorner.corner_trace_smul_eq line 81
  9. theorem OAI.KKConcreteCorner.corner_central_scalar line 89