OAI/RepresentationTheory/FoulkesSixth/StripCoefficient.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Foulkes.Strips.Composition line 11
  2. instance OAI.Foulkes.Strips.(instance at line 12) line 12
  3. def OAI.Foulkes.Strips.completePowers line 15
  4. def OAI.Foulkes.Strips.alternant line 19
  5. abbrev OAI.Foulkes.Strips.expVector line 22
  6. lemma OAI.Foulkes.Strips.expVector_apply line 24
  7. lemma OAI.Foulkes.Strips.exponent_injective line 27
  8. lemma OAI.Foulkes.Strips.coeff_complete_monomial line 37
  9. lemma OAI.Foulkes.Strips.perm_prod_monomial line 57
  10. lemma OAI.Foulkes.Strips.exists_composition_iff line 63
  11. lemma OAI.Foulkes.Strips.assignment_product line 95
  12. theorem OAI.Foulkes.Strips.coefficient_eq_assignment_det line 113
  13. theorem OAI.Foulkes.Strips.signed_strip_abs_le_one line 131