OAI/LinearAlgebra/MatrixMultiplication/FieldGroups/BranchLaws.lean
6 declarations, 0 contain sorry, 0 declared as axioms
Group assignments, orbit counts and extraction capacities.
- theorem
OAI.MatrixMultiplication.AllFieldGroupBranchLaws.jointCounts_branch_posline 16 - theorem
OAI.MatrixMultiplication.AllFieldGroupBranchLaws.branchLaw_stageA_mass_posline 27 - theorem
OAI.MatrixMultiplication.AllFieldGroupBranchLaws.branchLaw_stageB_mass_posline 33 - theorem
OAI.MatrixMultiplication.AllFieldGroupBranchLaws.supportedHalfLaw_branchShape_of_mass_posline 39 - theorem
OAI.MatrixMultiplication.AllFieldGroupBranchLaws.supportedHalfLaw_branchShape_of_mass_ne_zeroline 53 - theorem
OAI.MatrixMultiplication.AllFieldGroupBranchLaws.weighted_supportedHalfLaw_branchShapeline 64