OAI/RepresentationTheory/Saxl/TableauTransport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Saxl.tableauMove line 11

   Source comment

   A change of tableau enumeration only applies a position permutation.

   def tableauMove {n : ℕ} {μ : YoungDiagram} (s t : Tableau n μ) : Equiv.Perm (Fin n) :=
   …

   Mentions: OAI.Saxl.Tableau

2. lemma OAI.Saxl.tableauMove_apply line 14
3. lemma OAI.Saxl.tableauMove_inv_apply line 17
4. def OAI.Saxl.columnMove line 20
5. lemma OAI.Saxl.rowWord_move line 33
6. lemma OAI.Saxl.polytabloid_move line 39
7. lemma OAI.Saxl.polytabloid_mem_all line 68
8. lemma OAI.Saxl.spechtSub_tableau_independent line 73