OAI/RepresentationTheory/Saxl/BandOrbit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Saxl.sumPerm_mul line 13
2. lemma OAI.Saxl.sumPerm_one line 21
3. lemma OAI.Saxl.sumPerm_inv line 28
4. def OAI.Saxl.bandOrbitMap line 35
5. lemma OAI.Saxl.bandOrbitMap_base line 50
6. lemma OAI.Saxl.bandOrbitMap_nonzero line 68
7. lemma OAI.Saxl.bandOrbitMap_equivariant line 87