OAI/RepresentationTheory/UniversalSquare/Specht/YoungConverse.lean
5 declarations, 0 contain sorry, 0 declared as axioms
Young Converse.
- lemma
OAI.Saxl.rowPrefix_eq_countline 15 - lemma
OAI.Saxl.rowPrefix_eq_sum_indicatorline 25 - theorem
OAI.Saxl.dominates_of_mixedline 31 - theorem
OAI.Saxl.dominates_of_tabloid_homline 57 - theorem
OAI.Saxl.tabloid_supportLEline 77