OAI/Analysis/BoundedHochschild/HomogeneousTypeI.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The abelian commutant of a finite homogeneous type I matrix system.

  1. lemma OAI.HochschildMatrixSystems.MatrixSystem.commutant_central line 16
  2. lemma OAI.HochschildMatrixSystems.MatrixSystem.commutant_commutative_of_abelian_diagonal line 29