OAI/Probability/BinarySweep/YoungTheory/YoungSpecht.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryCoordinateSweeps.Young.polyModule line 15
  2. def OAI.BinaryCoordinateSweeps.Young.antiModule line 18
  3. lemma OAI.BinaryCoordinateSweeps.Young.antiModule_apply line 22
  4. lemma OAI.BinaryCoordinateSweeps.Young.antiModule_rank_one line 26
  5. lemma OAI.BinaryCoordinateSweeps.Young.antiModule_poly line 33
  6. def OAI.BinaryCoordinateSweeps.Young.Specht line 37
  7. lemma OAI.BinaryCoordinateSweeps.Young.polyModule_mem_Specht line 40
  8. lemma OAI.BinaryCoordinateSweeps.Young.polyModule_ne_zero line 43
  9. lemma OAI.BinaryCoordinateSweeps.Young.Specht_ne_bot line 49
  10. lemma OAI.BinaryCoordinateSweeps.Young.antiModule_mem line 55
  11. lemma OAI.BinaryCoordinateSweeps.Young.scalar_polyModule_mem_iff line 70
  12. lemma OAI.BinaryCoordinateSweeps.Young.Specht_le_iff line 74
  13. theorem OAI.BinaryCoordinateSweeps.Young.Specht_isAtom line 79
  14. instance OAI.BinaryCoordinateSweeps.Young.Specht_isSimpleModule line 109
  15. def OAI.BinaryCoordinateSweeps.Young.restrictLinearEquiv line 123
  16. abbrev OAI.BinaryCoordinateSweeps.Young.SpechtSpace line 130
  17. instance OAI.BinaryCoordinateSweeps.Young.SpechtSpace.instAddCommGroup line 133

    Source comment

    Use the same additive monoid for the restricted module and its additive group.
    instance SpechtSpace.instAddCommGroup : AddCommGroup (SpechtSpace μ) :=
…

    Mentions: OAI.BinaryCoordinateSweeps.Young.SpechtSpace

  18. instance OAI.BinaryCoordinateSweeps.Young.(instance at line 136) line 136
  19. def OAI.BinaryCoordinateSweeps.Young.spechtRep line 139
  20. instance OAI.BinaryCoordinateSweeps.Young.(instance at line 141) line 141
  21. instance OAI.BinaryCoordinateSweeps.Young.(instance at line 144) line 144
  22. instance OAI.BinaryCoordinateSweeps.Young.(instance at line 147) line 147
  23. def OAI.BinaryCoordinateSweeps.Young.spechtInclude line 150
  24. lemma OAI.BinaryCoordinateSweeps.Young.spechtInclude_injective line 155
  25. lemma OAI.BinaryCoordinateSweeps.Young.spechtInclude_rep line 159
  26. def OAI.BinaryCoordinateSweeps.Young.spechtPoly line 169
  27. lemma OAI.BinaryCoordinateSweeps.Young.spechtInclude_poly line 173
  28. lemma OAI.BinaryCoordinateSweeps.Young.spechtPoly_ne_zero line 181