OAI/Probability/SignedSweeps/SignedWords.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedSweeps.wordEvenSites_comp_mem line 14
  2. def OAI.SignedSweeps.oddPositionSetEquiv line 19
  3. def OAI.SignedSweeps.oddPositionEquiv line 27
  4. lemma OAI.SignedSweeps.oddPositionEquiv_one line 33
  5. lemma OAI.SignedSweeps.oddPositionEquiv_mul line 39
  6. def OAI.SignedSweeps.wordPhase line 46
  7. lemma OAI.SignedSweeps.wordPhase_one line 49
  8. lemma OAI.SignedSweeps.wordPhase_mul line 54
  9. lemma OAI.SignedSweeps.wordPhase_norm line 59
  10. def OAI.SignedSweeps.signedWordLinear line 62
  11. lemma OAI.SignedSweeps.signedWordLinear_apply line 68
  12. def OAI.SignedSweeps.signedWordRepresentation line 72
  13. lemma OAI.SignedSweeps.signedWordRepresentation_apply line 81
  14. lemma OAI.SignedSweeps.signedWordRepresentation_norm line 85
  15. lemma OAI.SignedSweeps.wordEvenSites_comp_eq line 93
  16. lemma OAI.SignedSweeps.oddPositionSetEquiv_sign_congr line 99
  17. lemma OAI.SignedSweeps.wordPhase_eq_of_parity line 108