OAI/Analysis/MatrixSigning/Matrices/Pivot.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W07.scalarPivot line 13
  2. def OAI.KS.W07.pivotRow line 15
  3. def OAI.KS.W07.pivotBlock line 17
  4. def OAI.KS.W07.pivotSchur line 21
  5. def OAI.KS.W07.pivotLower line 24
  6. def OAI.KS.W07.pivotDiagonal line 27
  7. def OAI.KS.W07.scalarPivotInvertible line 32
  8. theorem OAI.KS.W07.scalarPivot_inv line 43
  9. theorem OAI.KS.W07.pivot_ldl line 48
  10. def OAI.KS.W07.pivotWitnessLift line 71
  11. theorem OAI.KS.W07.pivot_schur_formula line 79
  12. theorem OAI.KS.W07.pivot_lift_cancel line 88
  13. theorem OAI.KS.W07.pivotWitnessLift_quadratic line 97