OAI/Combinatorics/Progressions/Geometry/CubicBoxStepDrop.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicBoxComponent line 18
  2. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicBoxComponent_eval line 24
  3. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicBoxComponent_vertical line 34
  4. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicKernelFactors line 44
  5. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicKernelFrequencies line 49
  6. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicKernelFactors_complexity line 52
  7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicKernelFactors_eval line 65
  8. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicKernelFactors_vertical line 72
  9. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicBoxCorner line 101
  10. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicBoxConjugated line 105
  11. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicAntisymmetricBoxValue line 110
  12. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicAntisymmetricBoxFactors line 116
  13. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicAntisymmetricBoxFrequencies line 122
  14. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicAntisymmetricBoxFactors_complexity line 125
  15. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicAntisymmetricBoxFactors_eval line 131
  16. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicAntisymmetricBoxFactors_vertical line 156
  17. def OAI.Erdos3.NativeMultidegreeNilcharacter.cubicAntisymmetricBoxNiltest line 174
  18. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicAntisymmetricBoxNiltest_complexity line 181
  19. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicAntisymmetricBoxNiltest_eval line 188
  20. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicAntisymmetricBoxNiltest_vertical line 194
  21. theorem OAI.Erdos3.exists_cubic_antisymmetric_box line 220
  22. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicAntisymmetricBoxValue_mean line 304
  23. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.cubicAntisymmetricBoxNiltest_mean line 339
  24. structure OAI.Erdos3.NativeCubicBoxFactorization line 363
  25. theorem OAI.Erdos3.exists_cubic_box_step_drop_indices line 384