OAI/LinearAlgebra/MatrixMultiplication/FieldGroups/Degrees.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Group assignments, orbit counts and extraction capacities.

  1. abbrev OAI.MatrixMultiplication.AllFieldGroupDegrees.Letter line 23
  2. abbrev OAI.MatrixMultiplication.AllFieldGroupDegrees.Class line 26
  3. abbrev OAI.MatrixMultiplication.AllFieldGroupDegrees.Symbol line 28
  4. def OAI.MatrixMultiplication.AllFieldGroupDegrees.projectedStatistic line 31
  5. def OAI.MatrixMultiplication.AllFieldGroupDegrees.classDesignated line 35
  6. def OAI.MatrixMultiplication.AllFieldGroupDegrees.classLaw line 39
  7. theorem OAI.MatrixMultiplication.AllFieldGroupDegrees.tripleSide_eq_sideWord line 43
  8. theorem OAI.MatrixMultiplication.AllFieldGroupDegrees.tripleSide_triple line 49
  9. theorem OAI.MatrixMultiplication.AllFieldGroupDegrees.childWidth_le line 56
  10. theorem OAI.MatrixMultiplication.AllFieldGroupDegrees.fineCompatible_uniform line 66
  11. def OAI.MatrixMultiplication.AllFieldGroupDegrees.uniformCompatible line 84
  12. theorem OAI.MatrixMultiplication.AllFieldGroupDegrees.Compatible_uniform line 95
  13. def OAI.MatrixMultiplication.AllFieldGroupDegrees.conditionalCount line 112
  14. theorem OAI.MatrixMultiplication.AllFieldGroupDegrees.uniformCompatible_count line 121
  15. theorem OAI.MatrixMultiplication.AllFieldGroupDegrees.competitors_card_le_conditionalCount line 133
  16. theorem OAI.MatrixMultiplication.AllFieldGroupDegrees.eligibility_card_le_sharedAmbient line 158