OAI/Probability/ThorpShuffle/Specht.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Thorp.Specht.perm_apply_inv line 18
  2. lemma OAI.Thorp.Specht.perm_inv_apply line 21
  3. def OAI.Thorp.Specht.Tabloid line 23

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

  4. instance OAI.Thorp.Specht.tabloidFinite line 25

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

  5. instance OAI.Thorp.Specht.tabloidFintype line 30

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

  6. instance OAI.Thorp.Specht.tabloidAction line 32

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

  7. lemma OAI.Thorp.Specht.tabloid_smul_apply line 46
  8. def OAI.Thorp.Specht.baseTabloid line 49

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

  9. lemma OAI.Thorp.Specht.baseTabloid_apply line 52
  10. def OAI.Thorp.Specht.fiberGroup line 54

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

  11. lemma OAI.Thorp.Specht.stabilizes_tabloid_iff line 66
  12. lemma OAI.Thorp.Specht.swap_preserves line 79
  13. def OAI.Thorp.Specht.complexSign line 88

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

  14. lemma OAI.Thorp.Specht.complexSign_conj line 93
  15. lemma OAI.Thorp.Specht.complexSign_inv line 96
  16. lemma OAI.Thorp.Specht.complexSign_swap line 99
  17. def OAI.Thorp.Specht.tableauRow line 104

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

  18. def OAI.Thorp.Specht.tableauCol line 106

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

  19. lemma OAI.Thorp.Specht.row_col_free line 110
  20. lemma OAI.Thorp.Specht.collision_odd line 121
  21. lemma OAI.Thorp.Specht.collision_or_column line 128
  22. def OAI.Thorp.Specht.tabloidRep line 166

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

  23. def OAI.Thorp.Specht.columnAlternator line 169

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

  24. def OAI.Thorp.Specht.polytabloid line 173

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

  25. lemma OAI.Thorp.Specht.polytabloid_support line 176
  26. lemma OAI.Thorp.Specht.polytabloid_diag line 194
  27. lemma OAI.Thorp.Specht.polytabloid_ne_zero line 199
  28. lemma OAI.Thorp.Specht.columnAlternator_rank_one line 208
  29. def OAI.Thorp.Specht.module line 215

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

  30. theorem OAI.Thorp.Specht.irreducible line 217