OAI/Probability/ThorpShuffle/Cyclic.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Thorp.Specht.cyclic line 17

    Also declared: ComparatorChallenges/ThorpFirstReciprocal.lean:69 (same declaration text).

  2. lemma OAI.Thorp.Specht.self_mem_cyclic line 31
  3. theorem OAI.Thorp.Specht.submodule_alternative line 34
  4. theorem OAI.Thorp.Specht.cyclic_irreducible line 65
  5. def OAI.Thorp.Specht.PermutationSpace.rep line 106

    Distinct definitions of this name: ComparatorChallenges/ThorpFirstReciprocal.lean:87 (same statement text; different proof or body). Qualify references as OAI.Thorp.Specht.PermutationSpace.rep@path.

  6. lemma OAI.Thorp.Specht.PermutationSpace.rep_apply line 119
  7. lemma OAI.Thorp.Specht.PermutationSpace.rep_unitary line 122
  8. lemma OAI.Thorp.Specht.PermutationSpace.rep_single line 128
  9. def OAI.Thorp.Specht.PermutationSpace.alternator line 136

    Distinct definitions of this name: ComparatorChallenges/ThorpFirstReciprocal.lean:101 (same statement text; different proof or body). Qualify references as OAI.Thorp.Specht.PermutationSpace.alternator@path.

  10. lemma OAI.Thorp.Specht.PermutationSpace.alternator_apply line 140
  11. lemma OAI.Thorp.Specht.PermutationSpace.alternator_stable line 145
  12. lemma OAI.Thorp.Specht.PermutationSpace.alternator_translate line 152
  13. lemma OAI.Thorp.Specht.PermutationSpace.alternator_single_zero line 169
  14. lemma OAI.Thorp.Specht.PermutationSpace.alternator_coeff line 180
  15. lemma OAI.Thorp.Specht.PermutationSpace.polytabloid_base line 185
  16. lemma OAI.Thorp.Specht.PermutationSpace.polytabloid_inner line 199
  17. theorem OAI.Thorp.Specht.PermutationSpace.alternator_rank_one line 210