OAI/Analysis/MatrixSigning/Matrices/UniformElimination.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KS.W17.schurTail_zero_pivot line 10
2. theorem OAI.KS.W17.schurWitnessLift_zero_pivot line 16
3. def OAI.KS.W17.pivotTerminal line 21
4. def OAI.KS.W17.uniformNegativeWitness line 28
5. theorem OAI.KS.W17.uniformNegativeWitness_eq line 35
6. inductive OAI.KS.W17.PivotHistory line 54
7. def OAI.KS.W17.PivotHistory.restore line 61
8. def OAI.KS.W17.PivotHistory.depth line 65
9. theorem OAI.KS.W17.PivotHistory.dimension_depth line 69
10. theorem OAI.KS.W17.PivotHistory.restore_push line 74
11. theorem OAI.KS.W17.PivotHistory.descent_restore line 78