OAI/Analysis/Pureness/States/ScalarMatrixTrace.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.TracialState.toPositiveQuasitrace line 11
  2. lemma OAI.CuntzPureness.TracialState.toPositiveQuasitrace_unit line 23
  3. lemma OAI.CuntzPureness.TracialState.toPositiveQuasitrace_add line 28
  4. lemma OAI.CuntzPureness.TracialState.toPositiveQuasitrace_sqrt_add line 33
  5. lemma OAI.CuntzPureness.TracialState.toPositiveQuasitrace_metricSize_add line 43
  6. def OAI.CuntzPureness.complexScalarTracialState line 70
  7. def OAI.CuntzPureness.scalarMatrixTracialState line 75
  8. def OAI.CuntzPureness.scalarMatrixPositiveTrace line 78
  9. lemma OAI.CuntzPureness.scalarMatrixPositiveTrace_unit line 81
  10. lemma OAI.CuntzPureness.scalarMatrixPositiveTrace_complex line 84
  11. lemma OAI.CuntzPureness.scalarMatrixPositiveTrace_metricSize_add line 91
  12. lemma OAI.CuntzPureness.scalarMatrixPositiveTrace_sqrt_add line 96