OAI/Analysis/TracialSplitting/FullProjections.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Pureness.hereditary_complex_smul_mem line 22
  2. lemma OAI.Pureness.hereditary_realPart_mem line 32
  3. lemma OAI.Pureness.hereditary_imaginaryPart_mem line 38
  4. lemma OAI.Pureness.trace_selfAdjoint_im_zero line 45
  5. lemma OAI.Pureness.trace_zero_selfadjoint_split line 54
  6. theorem OAI.Pureness.exists_orthogonal_pair_hereditary line 81
  7. lemma OAI.Pureness.exists_orthogonal_family_with_reserve line 126
  8. theorem OAI.Pureness.small_hereditary_rank line 168
  9. lemma OAI.CurrentMain.small_positive line 198
  10. lemma OAI.CurrentMain.simple_starAlgHom_injective line 215
  11. lemma OAI.CurrentMain.ClosedSelfAdjointSpan.span_star_mem line 237
  12. def OAI.CurrentMain.ClosedSelfAdjointSpan.ideal line 251
  13. lemma OAI.CurrentMain.ClosedSelfAdjointSpan.ideal_coe line 261
  14. lemma OAI.CurrentMain.ClosedSelfAdjointSpan.quotientMap_g line 265
  15. lemma OAI.CurrentMain.ClosedSelfAdjointSpan.nontrivial_quotient line 272