OAI/Analysis/BoundedHochschild/MatrixBlockGroups.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite unitary groups for finite central partitions of a matrix algebra.

  1. lemma OAI.HochschildMatrixSystems.MatrixSystem.partition_coe_projection line 22
  2. lemma OAI.HochschildMatrixSystems.MatrixSystem.partition_coe_orthogonal line 28
  3. lemma OAI.HochschildMatrixSystems.MatrixSystem.partition_coe_sum line 32
  4. def OAI.HochschildMatrixSystems.MatrixSystem.matrixBlockHom line 35
  5. def OAI.HochschildMatrixSystems.MatrixSystem.matrixBlockSpan line 40
  6. lemma OAI.HochschildMatrixSystems.MatrixSystem.matrixBlock_entry_mem_span line 44
  7. lemma OAI.HochschildMatrixSystems.MatrixSystem.matrixBlock_refined_entry_mem_span line 51