OAI/Analysis/BoundedHochschild/MatrixSeeds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Diagonal matrix projections and the type-II condition.

  1. lemma OAI.HochschildMatrixSystems.MatrixSystem.diagonal_projection line 27
  2. lemma OAI.HochschildMatrixSystems.MatrixSystem.diagonal_trace line 32
  3. lemma OAI.HochschildMatrixSystems.MatrixSystem.mul_diagonal_trace line 38
  4. lemma OAI.HochschildMatrixSystems.MatrixSystem.diagonal_full line 45
  5. lemma OAI.HochschildMatrixSystems.abelian_trace_bound line 62
  6. lemma OAI.HochschildMatrixSystems.no_abelian_of_matrixSystems line 73
  7. lemma OAI.HochschildMatrixSystems.finite_of_faithful_trace line 94
  8. theorem OAI.HochschildMatrixSystems.typeII1_of_matrixSystems line 107