OAI/Probability/SignedSweeps/WordTwirl.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SignedSweeps.wordIntertwiner line 10
2. lemma OAI.SignedSweeps.wordIntertwiner_matrix line 15
3. def OAI.SignedSweeps.wordTensorOrbitHull line 20
4. theorem OAI.SignedSweeps.exists_word_scalar_twirl line 25
5. lemma OAI.SignedSweeps.trace_starProjection line 76
6. lemma OAI.SignedSweeps.trace_scalar_projection line 85
7. lemma OAI.SignedSweeps.positive_trace_isometric_copy line 93
8. lemma OAI.SignedSweeps.wordMatrix_trace line 116
9. lemma OAI.SignedSweeps.wordMatrix_projection_commute line 121