OAI/RepresentationTheory/PartialPermutation/Restriction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PartialPermutation.isotypic_restrict_of_fullyInvariant line 18
2. def OAI.PartialPermutation.restrictGroupModule line 49
3. lemma OAI.PartialPermutation.restrictGroupModule_smul line 52
4. lemma OAI.PartialPermutation.group_isotypic_restrict line 56
5. lemma OAI.PartialPermutation.restrictGroupModule_tower line 114
6. lemma OAI.PartialPermutation.subgroup_algebra_commute line 124