OAI/RepresentationTheory/PartialPermutation/Polytabloids.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartialPermutation.YoungTabloid.tabloidRep line 13
  2. lemma OAI.PartialPermutation.YoungTabloid.tabloidRep_apply line 26
  3. lemma OAI.PartialPermutation.YoungTabloid.tabloidRep_unitary line 30
  4. def OAI.PartialPermutation.YoungTabloid.antisym line 36
  5. lemma OAI.PartialPermutation.YoungTabloid.antisym_apply line 39
  6. lemma OAI.PartialPermutation.YoungTabloid.antisym_alternating line 43
  7. def OAI.PartialPermutation.YoungTabloid.delta line 57
  8. def OAI.PartialPermutation.YoungTabloid.polytabloid line 60
  9. lemma OAI.PartialPermutation.YoungTabloid.canonical_fix_iff line 63
  10. lemma OAI.PartialPermutation.YoungTabloid.polytabloid_canonical line 71
  11. lemma OAI.PartialPermutation.YoungTabloid.polytabloid_ne_zero line 80
  12. lemma OAI.PartialPermutation.YoungTabloid.polytabloid_alternating line 86
  13. lemma OAI.PartialPermutation.YoungTabloid.antisym_rank_one line 89
  14. lemma OAI.PartialPermutation.YoungTabloid.signC_conj line 101
  15. lemma OAI.PartialPermutation.YoungTabloid.antisym_selfadjoint line 104
  16. lemma OAI.PartialPermutation.YoungTabloid.inner_delta line 115
  17. lemma OAI.PartialPermutation.YoungTabloid.antisym_eq_inner line 118