OAI/Probability/SignedSweeps/AllocationSigns.lean
11 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SignedSweeps.complexEquivSign_permCongrline 14 - def
OAI.SignedSweeps.allocationBlockPermutationline 19 - lemma
OAI.SignedSweeps.allocationBlockPermutation_leftline 23 - lemma
OAI.SignedSweeps.allocationBlockPermutation_rightline 29 - lemma
OAI.SignedSweeps.allocationBlockPermutation_memline 35 - def
OAI.SignedSweeps.allocationOddIndexline 43 - lemma
OAI.SignedSweeps.allocationOddIndex_valline 47 - lemma
OAI.SignedSweeps.allocation_odd_permutationline 50 - lemma
OAI.SignedSweeps.wordPhase_allocation_internalline 63 - lemma
OAI.SignedSweeps.wordPhaseDiagonal_allocationline 76 - theorem
OAI.SignedSweeps.pairWordEmbedding_signed_internalline 92