OAI/Probability/SignedSweeps/IrreducibleClassification.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.columnStatistic line 14
  2. lemma OAI.SignedSweeps.row_column_transversal_statistic line 17
  3. lemma OAI.SignedSweeps.row_column_transversal_bound_of_statistic_eq line 33
  4. def OAI.SignedSweeps.columnPositionsEquiv line 60
  5. lemma OAI.SignedSweeps.colOf_fiber_card line 76
  6. lemma OAI.SignedSweeps.row_column_transversal_eq_of_statistic_eq line 80
  7. lemma OAI.SignedSweeps.specht_hom_generator_ne_zero line 107
  8. lemma OAI.SignedSweeps.specht_hom_transversal line 115
  9. lemma OAI.SignedSweeps.specht_hom_columnStatistic line 154
  10. lemma OAI.SignedSweeps.specht_equiv_shape_eq line 160
  11. theorem OAI.SignedSweeps.specht_hom_nonzero_shape_eq line 180
  12. lemma OAI.SignedSweeps.specht_hom_eq_zero_of_ne line 188
  13. def OAI.SignedSweeps.natPartitionOfDiagram line 194
  14. def OAI.SignedSweeps.diagramOfNatPartition line 201
  15. lemma OAI.SignedSweeps.natPartitionOfDiagram_diagramOfNatPartition line 210
  16. lemma OAI.SignedSweeps.diagramOfNatPartition_natPartitionOfDiagram line 220
  17. def OAI.SignedSweeps.partitionEquivNatPartition line 230
  18. def OAI.SignedSweeps.conjugacyDiagram line 236
  19. lemma OAI.SignedSweeps.conjugacyDiagram_injective line 245
  20. def OAI.SignedSweeps.quotientCharacter line 259
  21. lemma OAI.SignedSweeps.quotientCharacter_mk line 267
  22. def OAI.SignedSweeps.classCharacterPairing line 271
  23. lemma OAI.SignedSweeps.specht_classCharacterPairing line 278
  24. lemma OAI.SignedSweeps.specht_characters_linearIndependent line 296
  25. lemma OAI.SignedSweeps.specht_characters_span line 304
  26. theorem OAI.SignedSweeps.irreducible_equiv_specht line 317