OAI/Analysis/Commutator/MatrixVonNeumann.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.OperatorAmplification.matrixVonNeumann line 24
2. lemma OAI.Kadison.OperatorAmplification.mem_matrixVonNeumann line 27
3. lemma OAI.Kadison.OperatorAmplification.matrixUnit_mem line 43
4. lemma OAI.Kadison.OperatorAmplification.diagonal_mem_matrixVonNeumann line 49
5. lemma OAI.Kadison.OperatorAmplification.matrix_representation_mem line 56
6. lemma OAI.Kadison.OperatorAmplification.matrixVonNeumann_is_range line 70
7. lemma OAI.Kadison.OperatorAmplification.factor_matrixVonNeumann line 77