OAI/RepresentationTheory/TensorSquares/Candidate.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Self-conjugate Young diagrams with prescribed size.

  1. def OAI.UniversalTensorSquares.rectangle line 12
  2. lemma OAI.UniversalTensorSquares.mem_rectangle line 19
  3. def OAI.UniversalTensorSquares.candidateArm line 24
  4. def OAI.UniversalTensorSquares.candidate line 27
  5. lemma OAI.UniversalTensorSquares.mem_candidate line 30
  6. lemma OAI.UniversalTensorSquares.candidate_transpose line 38
  7. lemma OAI.UniversalTensorSquares.candidate_zero line 44
  8. def OAI.UniversalTensorSquares.rightCells line 50
  9. lemma OAI.UniversalTensorSquares.mem_rightCells line 54
  10. lemma OAI.UniversalTensorSquares.rightCells_card line 61
  11. lemma OAI.UniversalTensorSquares.candidate_cells line 73
  12. lemma OAI.UniversalTensorSquares.candidate_card line 83
  13. lemma OAI.UniversalTensorSquares.candidate_rowLen line 107
  14. lemma OAI.UniversalTensorSquares.candidate_colLen line 119
  15. theorem OAI.UniversalTensorSquares.candidate_size_and_self_conjugacy line 129