OAI/Probability/SignedSweeps/ProjectionTrace.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedSweeps.projectionSubrepresentation_norm line 16
2. lemma OAI.SignedSweeps.projectionSubrepresentation_fixed line 23
3. lemma OAI.SignedSweeps.projectionSubrepresentation_trace line 32
4. lemma OAI.SignedSweeps.specht_dimension_expansion line 62
5. lemma OAI.SignedSweeps.exists_nonzero_of_multiplicity_ne_zero line 71
6. theorem OAI.SignedSweeps.sector_positive_restriction line 81