OAI/RepresentationTheory/FoulkesSixth/SymPolynomial.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Foulkes.SymPolynomial.Poly line 15
  2. abbrev OAI.Foulkes.SymPolynomial.H line 16
  3. def OAI.Foulkes.SymPolynomial.linearPolynomial line 18
  4. lemma OAI.Foulkes.SymPolynomial.linearPolynomial_apply line 23
  5. lemma OAI.Foulkes.SymPolynomial.eval_linearPolynomial line 26
  6. def OAI.Foulkes.SymPolynomial.tensorPolynomial line 34
  7. lemma OAI.Foulkes.SymPolynomial.tensorPolynomial_tprod line 38
  8. def OAI.Foulkes.SymPolynomial.polynomial line 42
  9. lemma OAI.Foulkes.SymPolynomial.polynomial_power line 45
  10. lemma OAI.Foulkes.SymPolynomial.polynomial_eval line 49
  11. lemma OAI.Foulkes.SymPolynomial.polynomial_injective line 61
  12. lemma OAI.Foulkes.SymPolynomial.polynomial_range line 78
  13. def OAI.Foulkes.SymPolynomial.equiv line 91
  14. lemma OAI.Foulkes.SymPolynomial.equiv_coe line 95