OAI/Analysis/Commutator/MatrixAlgebraDensity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.OperatorAmplification.fullMatrixAlgebra line 31
2. lemma OAI.Kadison.OperatorAmplification.fullMatrixAlgebra_closed line 34
3. lemma OAI.Kadison.OperatorAmplification.entry_represented line 39
4. lemma OAI.Kadison.OperatorAmplification.mem_fullMatrixAlgebra_iff line 44
5. lemma OAI.Kadison.OperatorAmplification.diagonal_mem_fullMatrixAlgebra line 57
6. lemma OAI.Kadison.OperatorAmplification.matrixUnit_mem_fullMatrixAlgebra line 67
7. lemma OAI.Kadison.OperatorAmplification.bicommutant_fullMatrix_of_entries line 78