OAI/RepresentationTheory/FoulkesSixth/PolynomialSpan.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Foulkes.PolynomialSpan.mapCoeffs line 12
  2. lemma OAI.Foulkes.PolynomialSpan.coeff_mapCoeffs line 15
  3. lemma OAI.Foulkes.PolynomialSpan.mapCoeffs_monomial line 22
  4. lemma OAI.Foulkes.PolynomialSpan.mapCoeffs_add line 29
  5. lemma OAI.Foulkes.PolynomialSpan.eval_mapCoeffs line 34
  6. lemma OAI.Foulkes.PolynomialSpan.mapCoeffs_zero line 47
  7. lemma OAI.Foulkes.PolynomialSpan.mapCoeffs_smul line 52
  8. def OAI.Foulkes.PolynomialSpan.mapCoeffsLM line 57
  9. lemma OAI.Foulkes.PolynomialSpan.mapCoeffs_sum line 62
  10. lemma OAI.Foulkes.PolynomialSpan.mapCoeffs_pderiv line 67
  11. lemma OAI.Foulkes.PolynomialSpan.mapCoeffs_X_mul line 74
  12. lemma OAI.Foulkes.PolynomialSpan.homogeneous_mapCoeffs line 81
  13. theorem OAI.Foulkes.PolynomialSpan.coeff_mem_of_evaluations line 87
  14. theorem OAI.Foulkes.PolynomialSpan.prod_pow_mem_span_powers line 102
  15. theorem OAI.Foulkes.PolynomialSpan.homogeneous_eq_span_powers line 122
  16. theorem OAI.Foulkes.PolynomialSpan.prod_mem_span_products line 144
  17. theorem OAI.Foulkes.PolynomialSpan.prod_mem_span_range line 167