OAI/Analysis/MatrixSigning/Machines/SchurColumnLoop.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W07.SchurLoopState.columnBudget line 13
2. theorem OAI.KS.W07.SchurLoopState.columnTicks_le line 16
3. theorem OAI.KS.W07.SchurLoopState.column_body_polynomial line 51
4. theorem OAI.KS.W07.SchurLoopState.run_columns line 59
5. theorem OAI.KS.W07.SchurLoopState.columns_spec line 106