OAI/Analysis/BoundedHochschild/CentralMatrices.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Central matrix approximation of projections.

  1. def OAI.HochschildCentralComparison.MatrixSystem.conjugate line 25
  2. lemma OAI.HochschildCentralComparison.MatrixSystem.commute_colored_diagonal line 40
  3. theorem OAI.HochschildCentralComparison.exists_central_matrix_projection_approx line 53