OAI/Analysis/Commutator/FreeSymmetry15.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Kadison.ActualHilbertSum.insert line 33
  2. def OAI.Kadison.ActualHilbertSum.project line 35
  3. def OAI.Kadison.ActualHilbertSum.block line 37
  4. lemma OAI.Kadison.ActualHilbertSum.project_insert line 40
  5. lemma OAI.Kadison.ActualHilbertSum.norm_project_le line 48
  6. lemma OAI.Kadison.ActualHilbertSum.norm_block_le line 52
  7. lemma OAI.Kadison.ActualHilbertSum.block_adjoint line 63
  8. lemma OAI.Kadison.ActualHilbertSum.project_coordinates line 69
  9. lemma OAI.Kadison.ActualHilbertSum.ext_vectors line 82
  10. lemma OAI.Kadison.ActualHilbertSum.project_insert_ne line 88
  11. lemma OAI.Kadison.ActualHilbertSum.reduces_of_offdiagonal line 98
  12. lemma OAI.Kadison.ActualHilbertSum.adjoint_reduces_of_offdiagonal line 114
  13. lemma OAI.Kadison.ActualHilbertSum.map_ext line 126
  14. lemma OAI.Kadison.ActualHilbertSum.project_covariant line 146
  15. lemma OAI.Kadison.ActualHilbertSum.block_covariant line 161
  16. lemma OAI.Kadison.ActualHilbertSum.block_covariant_of_insert line 170
  17. lemma OAI.Kadison.ActualHilbertSum.project_covariant_of_adjoint line 177