OAI/Probability/SignedSweeps/BlockPermutations.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.sigmaPermutation line 10
  2. lemma OAI.SignedSweeps.sigmaPermutation_injective line 16
  3. lemma OAI.SignedSweeps.sigmaPermutation_single line 25
  4. theorem OAI.SignedSweeps.sign_sigmaPermutation line 41
  5. def OAI.SignedSweeps.blockPermutation line 69
  6. lemma OAI.SignedSweeps.blockPermutation_apply line 74
  7. lemma OAI.SignedSweeps.blockPermutation_injective line 81
  8. lemma OAI.SignedSweeps.blockPermutation_fiber line 87