OAI/LinearAlgebra/MatrixMultiplication/FieldGroups/Selection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Group assignments, orbit counts and extraction capacities.

  1. theorem OAI.MatrixMultiplication.AllFieldGroupSelection.selected_of_native_count_bound line 22
  2. theorem OAI.MatrixMultiplication.AllFieldGroupSelection.exists_threshold_eventually_selected line 79