OAI/LinearAlgebra/MatrixMultiplication/FieldGroups/DegreeLaws.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Group assignments, orbit counts and extraction capacities.

  1. def OAI.MatrixMultiplication.AllFieldGroupDegreeLaws.nativeLaw line 21
  2. theorem OAI.MatrixMultiplication.AllFieldGroupDegreeLaws.nativeLaw_bounds line 26
  3. theorem OAI.MatrixMultiplication.AllFieldGroupDegreeLaws.weighted_classLaw_eq_native line 33
  4. theorem OAI.MatrixMultiplication.AllFieldGroupDegreeLaws.compatible_iff_native line 47
  5. def OAI.MatrixMultiplication.AllFieldGroupDegreeLaws.nativeCount line 88
  6. theorem OAI.MatrixMultiplication.AllFieldGroupDegreeLaws.conditionalCount_eq_native line 97
  7. theorem OAI.MatrixMultiplication.AllFieldGroupDegreeLaws.competitors_card_le_nativeCount line 107
  8. theorem OAI.MatrixMultiplication.AllFieldGroupDegreeLaws.competitors_subset_eligibility_of_first line 115
  9. theorem OAI.MatrixMultiplication.AllFieldGroupDegreeLaws.eventually_eligibility_card_le line 128
  10. theorem OAI.MatrixMultiplication.AllFieldGroupDegreeLaws.eventually_first_competitors_card_le line 139