OAI/Combinatorics/Progressions/Nilpotent/AllocatedOriginalDegreeQuotientBinNiltest.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.originalDegreeRefilteredBinOrbit line 43
  2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.originalDegreeRefilteredBinOrbit_eval line 52
  3. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.originalDegreeRefilteredBinTest line 77
  4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.originalDegreeRefilteredBinTest_complexity line 80
  5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.originalDegreeRefilteredBinTest_normBound line 84
  6. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.originalDegreeBinFrozen line 88
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.originalDegreeRefilteredBinTest_eval line 99
  8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.originalDegreeRefilteredBinTest_positiveImage_on_slice line 123
  9. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.originalDegreeRefilteredBinNative line 152