OAI/Analysis/Commutator/HermitianAlphabet.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.MatrixAlphabet.letter line 22
2. lemma OAI.Kadison.MatrixAlphabet.star_letter line 25
3. lemma OAI.Kadison.MatrixAlphabet.trace_letter line 29
4. lemma OAI.Kadison.MatrixAlphabet.trace_mul_letter line 32
5. def OAI.Kadison.MatrixAlphabet.scale line 45
6. lemma OAI.Kadison.MatrixAlphabet.star_scale line 48
7. lemma OAI.Kadison.MatrixAlphabet.scale_sq line 52
8. def OAI.Kadison.MatrixAlphabet.normalizedLetter line 57
9. lemma OAI.Kadison.MatrixAlphabet.star_normalizedLetter line 59
10. lemma OAI.Kadison.MatrixAlphabet.trace_normalizedLetter line 63
11. lemma OAI.Kadison.MatrixAlphabet.normalized_trace_mul line 66