OAI/Combinatorics/Progressions/Polynomial/PositivePolynomialLayerBases.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.MultidegreeLieFiltration.positiveCoefficientLayer line 19
  2. theorem OAI.Erdos3.MultidegreeLieFiltration.mem_positiveCoefficientLayer line 23
  3. theorem OAI.Erdos3.MultidegreeLieFiltration.boxedPolynomial_positive line 35
  4. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialCoefficientEquiv line 50
  5. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialCoefficientEquiv_apply line 68
  6. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialBasis line 87
  7. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialBasis_repr line 91
  8. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialBasis_coefficient_self line 97
  9. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialBasis_coefficient_ne line 104
  10. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialBasis_monomial line 112
  11. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialSupport line 148
  12. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialSupport_eq_span line 151
  13. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialSupportedBasis line 171
  14. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialSupportedBasis_coe line 175
  15. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialBasis_bracket_coefficient_height line 199
  16. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialBasis_structure_height line 218
  17. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialBasis_evaluation line 234
  18. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDownsetIdeal_eq_support line 256
  19. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDownsetIdeal_eq_span line 260
  20. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDownsetBasis line 266
  21. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDownsetBasis_apply line 272
  22. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDownsetBasis_repr line 278
  23. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDownset_multidegree_span line 284
  24. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDownset_degree_span line 293
  25. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomial_downset_basis_cover line 319
  26. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDownsetCosetMap line 331
  27. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomial_downset_coset_pair_injective line 342
  28. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialQuotientProduct line 377
  29. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialQuotientProductMap line 380
  30. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialQuotientProductRealMap line 385
  31. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialQuotientProductLattice line 392
  32. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialQuotientProductRealMap_component line 400
  33. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomial_quotient_family_basis_cover line 415
  34. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialQuotientProductRealMap_injective line 435
  35. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialQuotientProduct_lattice_detect line 454
  36. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialQuotientProduct_lattice_cover line 477
  37. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDownsetMultidegreeBasis line 505
  38. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDownsetMultidegreeBasis_height line 513
  39. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDownsetDegreeBasis line 521
  40. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDownsetDegreeBasis_height line 529
  41. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialSupportedFinBasis line 553
  42. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialSupportedFinBasis_height line 559
  43. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialMultidegreeBasis line 567
  44. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialMultidegreeBasis_height line 572
  45. def OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDegreeBasis line 577
  46. theorem OAI.Erdos3.MultidegreeLieFiltration.positivePolynomialDegreeBasis_height line 582