OAI/Combinatorics/Progressions/Nilpotent/PositiveShiftTestingNiltests.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Erdos3.PositiveShiftBasis.testingNiltestline 17 - theorem
OAI.Erdos3.PositiveShiftBasis.testingNiltest_evalline 25 - theorem
OAI.Erdos3.PositiveShiftBasis.testingNiltest_normline 37 - theorem
OAI.Erdos3.PositiveShiftBasis.testingNiltest_complexityline 46