OAI/Analysis/TracialSplitting/HereditaryAlgebras.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Pureness.cstar_cuntzSubequiv_refl line 19
  2. def OAI.Pureness.positiveCuntzSetoid line 48
  3. def OAI.Pureness.PositiveCuntzClass line 55
  4. theorem OAI.Pureness.hereditary_cuntzSubequiv line 66
  5. lemma OAI.Pureness.norm_mul_star_self line 93
  6. lemma OAI.Pureness.tendsto_mul_zero_of_norm_le_one line 97
  7. lemma OAI.Pureness.normalizedRoot_mul_of_mul_star_self_tendsto line 108
  8. theorem OAI.Pureness.star_mul_self_cuntzSubequiv_of_hereditary line 137
  9. theorem OAI.Pureness.star_mul_self_cuntzSubequiv line 147
  10. theorem OAI.Pureness.mul_star_self_cuntzSubequiv line 151
  11. lemma OAI.Pureness.exists_nonzero_cross line 162
  12. theorem OAI.Pureness.exists_common_minorant line 177
  13. theorem OAI.Pureness.exists_finite_common_minorant line 210
  14. lemma OAI.Pureness.hereditary_mul_eq_zero line 246
  15. lemma OAI.Pureness.orthogonal_add_le_one line 262
  16. lemma OAI.Pureness.orthogonal_sum_le_one line 274
  17. theorem OAI.Pureness.orthogonal_rank_sum_le_one line 297
  18. theorem OAI.Pureness.small_rank_of_orthogonal_family line 327
  19. theorem OAI.Pureness.finiteDimensional_of_scalar_sandwich line 351
  20. theorem OAI.Pureness.exists_nonscalar_sandwich line 382