OAI/LinearAlgebra/MatrixMultiplication/FieldGroups/OrbitCount.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Group assignments, orbit counts and extraction capacities.

  1. abbrev OAI.MatrixMultiplication.AllFieldGroupOrbitCount.GroupClasses line 16
  2. abbrev OAI.MatrixMultiplication.AllFieldGroupOrbitCount.GroupPositions line 19
  3. abbrev OAI.MatrixMultiplication.AllFieldGroupOrbitCount.GroupLetters line 23
  4. abbrev OAI.MatrixMultiplication.AllFieldGroupOrbitCount.GroupOrbit line 26
  5. instance OAI.MatrixMultiplication.AllFieldGroupOrbitCount.groupOrbitFintype line 31
  6. def OAI.MatrixMultiplication.AllFieldGroupOrbitCount.groupDegree line 38
  7. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitCount.card_groupLetters line 41
  8. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitCount.groupClass_card_le line 46
  9. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitCount.card_groupOrbit_le line 52
  10. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitCount.card_groupOrbit_le_polynomial line 65
  11. def OAI.MatrixMultiplication.AllFieldGroupOrbitCount.groupOrbitPrefactor line 76
  12. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitCount.groupOrbitPrefactor_pos line 80
  13. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitCount.card_groupOrbit_le_polynomial_real line 85
  14. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitCount.usedGroupOrbits_card_le_real line 93
  15. theorem OAI.MatrixMultiplication.AllFieldGroupOrbitCount.taggedUsedGroupOrbits_card_le_real line 106