OAI/Combinatorics/Progressions/Geometry/MixedCoordinateTransfer.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NativeMultidegreeNilcharacter.boxComponent line 22
  2. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.boxComponent_eval line 28
  3. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.boxComponent_vertical line 35
  4. def OAI.Erdos3.NativeMultidegreeNilcharacter.antisymmetricBoxValue line 45
  5. def OAI.Erdos3.NativeMultidegreeNilcharacter.antisymmetricBoxFactors line 49
  6. def OAI.Erdos3.NativeMultidegreeNilcharacter.antisymmetricBoxFrequencies line 56
  7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.antisymmetricBoxFactors_complexity line 60
  8. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.antisymmetricBoxFactors_eval line 74
  9. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.antisymmetricBoxFactors_vertical line 79
  10. def OAI.Erdos3.NativeMultidegreeNilcharacter.antisymmetricBoxNiltest line 101
  11. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.antisymmetricBoxNiltest_complexity line 106
  12. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.antisymmetricBoxNiltest_eval line 111
  13. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.antisymmetricBoxNiltest_vertical line 116
  14. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.antisymmetricBoxValue_mean line 145
  15. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.antisymmetricBoxNiltest_mean line 184
  16. def OAI.Erdos3.NativeMultidegreeNilcharacter.antisymmetricKernel line 202
  17. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.antisymmetricKernel_norm line 207
  18. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.antisymmetricKernel_cyclic line 214
  19. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.antisymmetricKernel_box line 227
  20. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_coordinate_slice line 232
  21. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_antisymmetric_coordinate_slice line 262
  22. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_self_equivalence line 308
  23. def OAI.Erdos3.NativeMultidegreeNilcharacter.coordinateTransfer line 318
  24. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.antisymmetricKernel_tuple line 323
  25. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.coordinateTransfer_diagonal line 336
  26. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.coordinateTransfer_matrix_error line 342
  27. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_coordinate_transfer_expansions line 355