OAI/LinearAlgebra/MatrixMultiplication/FieldGroups/OrbitData.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Group assignments, orbit counts and extraction capacities.

  1. abbrev OAI.MatrixMultiplication.AllFieldGroupOrbitData.Counts line 24
  2. abbrev OAI.MatrixMultiplication.AllFieldGroupOrbitData.Targets line 26
  3. abbrev OAI.MatrixMultiplication.AllFieldGroupOrbitData.Pos line 28
  4. abbrev OAI.MatrixMultiplication.AllFieldGroupOrbitData.Raw line 30
  5. abbrev OAI.MatrixMultiplication.AllFieldGroupOrbitData.Orbit line 32
  6. abbrev OAI.MatrixMultiplication.AllFieldGroupOrbitData.Variable line 34
  7. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.tripleSide line 37
  8. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.reorder line 40
  9. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitData.tripleSide_reorder line 43
  10. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitData.reorder_injective line 48
  11. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitData.reorder_support line 52
  12. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.coarse line 56
  13. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.ambient line 60
  14. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.support line 65
  15. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitData.counts_support line 69
  16. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitData.coarse_injective line 75
  17. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitData.ambient_support line 79
  18. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitData.coarse_mem_ambient line 85
  19. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.sharing line 95
  20. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.workComplement line 101
  21. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.complement line 107
  22. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.compatibilityLaw line 110
  23. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.designated line 119
  24. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.fineCompatible line 128
  25. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.ownWord line 137
  26. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.Compatible line 141
  27. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.Admissible line 147
  28. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.orbitOf line 155
  29. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.usedOrbits line 160
  30. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.full line 165
  31. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.passing line 170
  32. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.competitors line 175
  33. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitData.full_pos line 184
  34. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitData.competitor_mem line 191
  35. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitData.competitor_shares line 199
  36. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.data line 210
  37. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitData.admissible_covered line 229
  38. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitData.orbits_card_le line 238
  39. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.actualCompatible line 245
  40. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.actualUseful line 250
  41. def OAI.MatrixMultiplication.AllFieldGroupOrbitData.actualKeep line 256
  42. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitData.actualCompatible_coarse line 260
  43. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitData.actualUseful_coarse line 270
  44. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitData.competitor_coverage line 280
  45. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitData.mem_passing line 295