OAI/Analysis/MatrixSigning/Optimization/SchurWitnessHead.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.KS.W12.RowDot.schurHeadline 11 - def
OAI.KS.W12.RowDot.fetchPivotProgramline 14 - def
OAI.KS.W12.RowDot.schurHeadProgramline 16 - def
OAI.KS.W12.RowDot.schurHeadTicksline 19 - theorem
OAI.KS.W12.RowDot.schurHead_specline 25 - theorem
OAI.KS.W12.RowDot.schurHeadTicks_storedline 58 - theorem
OAI.KS.W12.RowDot.schurHead_polynomial_specline 106