OAI/Probability/SignedSweeps/SignedBlockTrace.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedSweeps.groupWordEquiv_permutation line 14
  2. lemma OAI.SignedSweeps.group_parity_eq line 21
  3. def OAI.SignedSweeps.blockOddEquiv line 30
  4. theorem OAI.SignedSweeps.wordPhase_block_fixedParity line 53
  5. lemma OAI.SignedSweeps.signedWord_left_matrix line 90
  6. lemma OAI.SignedSweeps.signedWord_trace line 99
  7. lemma OAI.SignedSweeps.groupedPairTypeProjection_matrix line 117
  8. lemma OAI.SignedSweeps.groupedPairTypeProjection_local_parity_off line 127
  9. lemma OAI.SignedSweeps.groupedPairTypeProjection_parity_off line 135
  10. theorem OAI.SignedSweeps.grouped_signed_type_trace line 146
  11. lemma OAI.SignedSweeps.groupedPairTypeProjection_phase_commute line 178
  12. lemma OAI.SignedSweeps.groupedPairTypeProjection_permutation_commute line 192
  13. theorem OAI.SignedSweeps.groupedPairTypeProjection_signed_commute line 214