OAI/Probability/SignedSweeps/BlockPermutations.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SignedSweeps.sigmaPermutationline 10 - lemma
OAI.SignedSweeps.sigmaPermutation_injectiveline 16 - lemma
OAI.SignedSweeps.sigmaPermutation_singleline 25 - theorem
OAI.SignedSweeps.sign_sigmaPermutationline 41 - def
OAI.SignedSweeps.blockPermutationline 69 - lemma
OAI.SignedSweeps.blockPermutation_applyline 74 - lemma
OAI.SignedSweeps.blockPermutation_injectiveline 81 - lemma
OAI.SignedSweeps.blockPermutation_fiberline 87