OAI/Analysis/BoundedHochschild/MatrixAlgebras.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Finite matrix subalgebras and their commutants.

  1. def OAI.HochschildMatrixSystems.MatrixSystem.entrySpan line 22
  2. lemma OAI.HochschildMatrixSystems.MatrixSystem.entry_mem_span line 24
  3. lemma OAI.HochschildMatrixSystems.MatrixSystem.one_mem_entrySpan line 28
  4. lemma OAI.HochschildMatrixSystems.MatrixSystem.mul_mem_entrySpan line 32
  5. lemma OAI.HochschildMatrixSystems.MatrixSystem.star_mem_entrySpan line 51
  6. def OAI.HochschildMatrixSystems.MatrixSystem.matrixAlgebra line 61
  7. instance OAI.HochschildMatrixSystems.MatrixSystem.matrixAlgebra_finiteDimensional line 73
  8. instance OAI.HochschildMatrixSystems.MatrixSystem.matrixAlgebra_closed line 76
  9. lemma OAI.HochschildMatrixSystems.MatrixSystem.commutant_commutes_matrix line 80
  10. instance OAI.HochschildMatrixSystems.MatrixSystem.matrixUnitary_compactSpace line 92