OAI/Combinatorics/Progressions/Geometry/MixedBoxStepDrop.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos3.MixedBoxIndex line 10
  2. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedBoxComponent line 24
  3. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedBoxComponent_eval line 31
  4. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedBoxComponent_vertical line 42
  5. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedKernelFactors line 52
  6. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedKernelFrequencies line 57
  7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedKernelFactors_complexity line 60
  8. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedKernelFactors_normBound line 66
  9. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedKernelFactors_eval line 70
  10. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedKernelFactors_vertical line 78
  11. abbrev OAI.Erdos3.MixedBoxFactor line 100
  12. theorem OAI.Erdos3.mixedBoxFactor_card line 102
  13. def OAI.Erdos3.mixedBoxBudget line 107
  14. theorem OAI.Erdos3.mixedBoxFactor_card_le_budget line 109
  15. def OAI.Erdos3.mixedBoxCorner line 115
  16. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetricBoxValue line 128
  17. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetricBoxFactors line 131
  18. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetricBoxFrequencies line 136
  19. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetricBoxFactors_complexity line 139
  20. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetricBoxFactors_normBound line 145
  21. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetricBoxFactors_eval line 150
  22. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetricBoxValue_norm line 166
  23. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetricBoxFactors_vertical line 174
  24. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetricBoxNiltest line 192
  25. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetricBoxNiltest_complexity line 199
  26. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetricBoxNiltest_eval line 206
  27. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetricBoxNiltest_vertical line 212
  28. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetricBoxValue_mean line 245
  29. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedAntisymmetricBoxNiltest_mean line 255
  30. structure OAI.Erdos3.NativeMixedBoxFactorization line 277
  31. theorem OAI.Erdos3.exists_mixed_box_step_drop_indices line 297