OAI/Analysis/Commutator/MatrixStandardForm.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.OperatorAmplification.standardMatrixRepresentation line 27
2. lemma OAI.Kadison.OperatorAmplification.standardMatrixRepresentation_equiv line 31
3. lemma OAI.Kadison.OperatorAmplification.standardMatrixTrace_vector line 38
4. lemma OAI.Kadison.OperatorAmplification.standardMatrix_vacuum_cyclic line 42
5. def OAI.Kadison.OperatorAmplification.standardMatrixUnitary line 50
6. lemma OAI.Kadison.OperatorAmplification.standardMatrixUnitary_intertwines line 55
7. lemma OAI.Kadison.OperatorAmplification.standardMatrixUnitary_algebraVector line 61