OAI/Probability/SignedSweeps/RestrictionSum2.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.subdiagramLabels line 15
  2. lemma OAI.SignedSweeps.subdiagramLabels_row line 24
  3. lemma OAI.SignedSweeps.subdiagramLabels_col line 30
  4. def OAI.SignedSweeps.subdiagramEmbedding line 36
  5. lemma OAI.SignedSweeps.subdiagramEmbedding_row line 40
  6. lemma OAI.SignedSweeps.subdiagramEmbedding_col line 51
  7. lemma OAI.SignedSweeps.complexSign_viaEmbedding line 62
  8. theorem OAI.SignedSweeps.subdiagram_specht_occurs line 66
  9. def OAI.SignedSweeps.blockEmbeddingHom line 111
  10. lemma OAI.SignedSweeps.blockEmbeddingHom_apply line 117
  11. def OAI.SignedSweeps.blockSpinInjection line 121
  12. lemma OAI.SignedSweeps.blockEmbedding_one_remainder line 125
  13. lemma OAI.SignedSweeps.viaEmbedding_trans line 145
  14. lemma OAI.SignedSweeps.sumCongr_viaEmbedding line 168
  15. lemma OAI.SignedSweeps.viaEmbedding_conjugate line 206
  16. def OAI.SignedSweeps.spinRestriction line 226
  17. lemma OAI.SignedSweeps.spinRestriction_apply line 231
  18. theorem OAI.SignedSweeps.signed_occurrence_of_spin_intertwiner line 235
  19. theorem OAI.SignedSweeps.signed_occurrence_subdiagrams line 256
  20. lemma OAI.SignedSweeps.truncatePartition_le line 350
  21. lemma OAI.SignedSweeps.truncatePartition_length line 363
  22. def OAI.SignedSweeps.truncatedRemainder line 368
  23. lemma OAI.SignedSweeps.truncated_size_eq line 371
  24. theorem OAI.SignedSweeps.signed_occurrence_truncate line 381
  25. theorem OAI.SignedSweeps.signed_moment_of_bounded_lengths line 390