OAI/Analysis/KadisonSimilarity/Tracial/MatrixGNSNormality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The native matrix GNS representation has normal range whenever the original native GNS representation does.

  1. theorem OAI.KadisonSimilarity.matrix_gns_normal_range line 21
  2. theorem OAI.KadisonSimilarity.matrix_trace_balls_closed line 40