OAI/Combinatorics/Progressions/Linear/WeightedTranslationOrderedBasis.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.PolynomialTranslationLie.weightedIndexOrder line 14
  2. def OAI.Erdos3.PolynomialTranslationLie.weightedOrderedBasis line 20
  3. def OAI.Erdos3.PolynomialTranslationLie.weightedOrderedGrade line 24
  4. theorem OAI.Erdos3.PolynomialTranslationLie.weightedOrderedGrade_monotone line 28
  5. theorem OAI.Erdos3.PolynomialTranslationLie.weightedOrderedGrade_pos line 33
  6. theorem OAI.Erdos3.PolynomialTranslationLie.weightedOrderedGrade_le line 37
  7. theorem OAI.Erdos3.PolynomialTranslationLie.weightedOrderedBasis_layers line 41
  8. theorem OAI.Erdos3.PolynomialTranslationLie.weightedOrderedBasis_central line 49
  9. def OAI.Erdos3.PolynomialTranslationLie.weightedLayerBasis line 55
  10. theorem OAI.Erdos3.PolynomialTranslationLie.weightedLayerBasis_height line 61
  11. def OAI.Erdos3.PolynomialTranslationLie.weightedLayerIndexEquiv line 68
  12. def OAI.Erdos3.PolynomialTranslationLie.weightedLayerFinBasis line 74
  13. theorem OAI.Erdos3.PolynomialTranslationLie.weightedLayerFinBasis_height line 79
  14. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasisIndex_card_le line 86
  15. theorem OAI.Erdos3.PolynomialTranslationLie.weightedOrderedBasis_repr line 91
  16. theorem OAI.Erdos3.PolynomialTranslationLie.weightedOrderedBasis_structure_height line 97
  17. theorem OAI.Erdos3.PolynomialTranslationLie.weightedOrderedBasis_structure_height_succ line 102