OAI/Analysis/Commutator/AmplifiedTowerStage.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.OperatorAmplification.matrixUnit_mul line 25
2. lemma OAI.Kadison.OperatorAmplification.matrixUnit_star line 33
3. lemma OAI.Kadison.OperatorAmplification.sum_matrixUnit line 50
4. def OAI.Kadison.OperatorAmplification.scalarMatrixHom line 54
5. lemma OAI.Kadison.OperatorAmplification.scalarMatrixHom_single line 70
6. lemma OAI.Kadison.OperatorAmplification.scalarMatrixHom_coe line 74
7. lemma OAI.Kadison.OperatorAmplification.scalar_diagonal_commute line 82
8. def OAI.Kadison.OperatorAmplification.amplifiedStage line 95
9. lemma OAI.Kadison.OperatorAmplification.amplifiedStage_scalar line 103
10. lemma OAI.Kadison.OperatorAmplification.amplifiedStage_diagonal line 111