OAI/Combinatorics/Progressions/Nilpotent/NativeIntegerChartNiltest.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.integerSampledRealChart_freeze_support line 9
  2. def OAI.Erdos3.RationalFilteredNilmanifold.Niltest.integerChartPullback line 37
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.integerChartPullback_orbit line 40
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.integerChartPullback_observable line 44
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.integerChartPullback_normBound line 47
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.integerChartPullback_lipBound line 50
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.integerChartPullback_complexity line 53
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.integerChartPullback_complexity_of line 56
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.integerChartPullback_unitIntervalValued line 59
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.integerChartPullback_eval line 62
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.integerChartPullback_vertical line 74
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.integerChartPullback_polynomialCoordinates line 84
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.integerChartPullback_orbit_eq_of_orbit_eq line 98
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.integerChartPullback_symbol line 103
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.integerChartPullback_frozen_symbol_independent line 114