OAI/Probability/BinarySweep/YoungTheory/CoindFibers.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.Irrep.cosetEquiv line 22
2. lemma OAI.BinaryCoordinateSweeps.Irrep.cosetEquiv_symm_mul line 24
3. lemma OAI.BinaryCoordinateSweeps.Irrep.cosetEquiv_symm_rep line 33
4. def OAI.BinaryCoordinateSweeps.Irrep.coindFiberInverse line 38
5. def OAI.BinaryCoordinateSweeps.Irrep.coindFiberEquiv line 45
6. lemma OAI.BinaryCoordinateSweeps.Irrep.coindFiberEquiv_action line 61
7. lemma OAI.BinaryCoordinateSweeps.Irrep.placement_cosets_bijective line 73
8. lemma OAI.BinaryCoordinateSweeps.Irrep.cosetIndex_mul line 110
9. def OAI.BinaryCoordinateSweeps.Irrep.cosetIndexAction line 118
10. abbrev OAI.BinaryCoordinateSweeps.Irrep.CoindHilbertSpace line 124
11. def OAI.BinaryCoordinateSweeps.Irrep.coindHilbertEquiv line 126
12. def OAI.BinaryCoordinateSweeps.Irrep.coindHilbertRep line 129
13. lemma OAI.BinaryCoordinateSweeps.Irrep.coindHilbertEquiv_apply line 135
14. lemma OAI.BinaryCoordinateSweeps.Irrep.coindHilbertRep_apply line 139
15. lemma OAI.BinaryCoordinateSweeps.Irrep.coindHilbert_unitary line 150
16. def OAI.BinaryCoordinateSweeps.Irrep.homCongr line 171
17. lemma OAI.BinaryCoordinateSweeps.Irrep.multiplicity_congr line 194
18. def OAI.BinaryCoordinateSweeps.Irrep.repEquiv_comp line 198