OAI/Combinatorics/Progressions/Nilpotent/PolynomialShearNilmanifold.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.polynomialShearLayerBasis line 14
  2. theorem OAI.Erdos3.polynomialShearLayerBasis_height line 20
  3. def OAI.Erdos3.polynomialShearLayerIndexEquiv line 27
  4. def OAI.Erdos3.polynomialShearLayerFinBasis line 33
  5. theorem OAI.Erdos3.polynomialShearLayerFinBasis_height line 38
  6. def OAI.Erdos3.polynomialShearNilmanifold line 44
  7. theorem OAI.Erdos3.polynomialShearNilmanifold_complexity line 56
  8. theorem OAI.Erdos3.polynomialShearNilmanifold_complexity_budget line 69