OAI/LinearAlgebra/MatrixFields/Extraction/ComplexFiniteSeparation.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.grid_modular_collision line 13
  2. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.squaredNorm line 28
  3. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.dot line 30
  4. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.squaredNorm_displacement line 32
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.sphere_slice_collision line 47
  6. abbrev OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.Grid line 75
  7. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.gridSquaredNorm line 77
  8. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.gridDot line 79
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.gridSquaredNorm_le line 81
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.gridDot_le line 89
  11. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.normColor line 98
  12. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.dotColor line 101
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.two_stage_pigeonhole line 104
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.grid_tags_slices line 126
  15. abbrev OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.AuxiliaryGroup line 143
  16. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.gridToGroup line 145
  17. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.gridToReal line 148
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.gridToReal_injective line 151
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.squaredNorm_gridToReal line 160
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.dot_gridToReal line 164
  21. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.grid_group_collision_lift line 168
  22. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.grid_sphere_slice_collision line 189
  23. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.indexed_grid_collision line 213
  24. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.exists_modular_separation line 231
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Separation.card_auxiliaryGroup line 272
  26. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.separatedTensor line 290
  27. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.finite_separation_identity line 295
  28. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.finite_separation_mem_restrictionOrbit line 313
  29. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.finite_separation_degeneratesTo line 332
  30. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.finite_separation_rankAtMost line 344
  31. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.finite_separation_borderRankAtMost line 355
  32. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.finite_grid_separation_mem_restrictionOrbit line 376
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.finite_grid_separation_rankAtMost line 396
  34. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.finite_grid_separation_borderRankAtMost line 417