OAI/Probability/ThorpShuffle/SymmetricFamilies.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Thorp.Specht.family_unitaryline 14 - lemma
OAI.Thorp.Specht.regular_char_finline 19 - def
OAI.Thorp.Specht.symmetricFamilyline 28 - def
OAI.Thorp.Fourier.subrepPullline 52 - def
OAI.Thorp.Fourier.Family.pullline 65