OAI/RepresentationTheory/PartialPermutation/ComponentGeometry.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartialPermutation.componentSpace line 19
2. lemma OAI.PartialPermutation.componentSpace_invariant line 23
3. lemma OAI.PartialPermutation.iSup_componentSpace line 31
4. lemma OAI.PartialPermutation.componentSpace_projection_commute line 37
5. lemma OAI.PartialPermutation.componentSpace_orthogonal line 52
6. lemma OAI.PartialPermutation.sum_component_projections line 72
7. lemma OAI.PartialPermutation.sum_component_norm_sq line 79