OAI/RepresentationTheory/PartialPermutation/AlternatingTabloids.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartialPermutation.YoungTabloid.signC line 13
2. lemma OAI.PartialPermutation.YoungTabloid.signC_one line 16
3. lemma OAI.PartialPermutation.YoungTabloid.signC_mul line 18
4. lemma OAI.PartialPermutation.YoungTabloid.signC_inv line 20
5. lemma OAI.PartialPermutation.YoungTabloid.signC_sq line 22
6. lemma OAI.PartialPermutation.YoungTabloid.signC_swap line 25
7. lemma OAI.PartialPermutation.YoungTabloid.swap_mem_column line 28
8. lemma OAI.PartialPermutation.YoungTabloid.relabel_swap_fix line 37
9. def OAI.PartialPermutation.YoungTabloid.Alternating line 49
10. lemma OAI.PartialPermutation.YoungTabloid.alternating_zero_nontransversal line 52
11. lemma OAI.PartialPermutation.YoungTabloid.relabel_canonical line 63
12. lemma OAI.PartialPermutation.YoungTabloid.column_canonical_injective line 66
13. lemma OAI.PartialPermutation.YoungTabloid.transversal_column_orbit line 72
14. lemma OAI.PartialPermutation.YoungTabloid.alternating_eq_of_canonical_eq line 79