OAI/RepresentationTheory/Saxl/DominatedSupport.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Saxl.transpose_card line 13
2. def OAI.Saxl.colTruncate line 17
3. lemma OAI.Saxl.colTruncate_rowLen line 19
4. lemma OAI.Saxl.colTruncate_height line 34
5. lemma OAI.Saxl.sum_range_if_lt line 42
6. lemma OAI.Saxl.corner_inequality line 51
7. lemma OAI.Saxl.corner_equality line 70
8. theorem OAI.Saxl.dominates_transpose line 97

   Source comment

   Ordinary conjugation reverses dominance, including empty diagrams.

   theorem dominates_transpose {μ ν : YoungDiagram} (hc : μ.card = ν.card)
       (h : Dominates μ ν) : Dominates ν.transpose μ.transpose := by
   …

   Mentions: OAI.Saxl.Dominates

9. lemma OAI.Saxl.rowWord_content line 111
10. lemma OAI.Saxl.staircase_transpose line 135
11. def OAI.Saxl.signCancelMap line 143
12. theorem OAI.Saxl.dominated_support line 158