OAI/NumberTheory/Catalan/FiniteMatrices/FixedGaussianPivots.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.fixedGaussianSwap line 12
  2. def OAI.InternalCatalan.fixedGaussianStep line 16
  3. def OAI.InternalCatalan.fixedGaussianPivot line 21
  4. theorem OAI.InternalCatalan.fixedGaussianPivot_unique line 25
  5. theorem OAI.InternalCatalan.fixedGaussianStep_pivot_row line 33
  6. def OAI.InternalCatalan.fixedGaussianTrace line 37
  7. def OAI.InternalCatalan.fixedGaussianZeroPivots line 52
  8. def OAI.InternalCatalan.fixedGaussianZeroRows line 104
  9. theorem OAI.InternalCatalan.fixedGaussianZeroPivots_nonzero line 107
  10. def OAI.InternalCatalan.fixedGaussianPlusPivots line 111
  11. def OAI.InternalCatalan.fixedGaussianPlusRows line 163
  12. theorem OAI.InternalCatalan.fixedGaussianPlusPivots_nonzero line 166
  13. def OAI.InternalCatalan.fixedGaussianMinusPivots line 170
  14. def OAI.InternalCatalan.fixedGaussianMinusRows line 222
  15. theorem OAI.InternalCatalan.fixedGaussianMinusPivots_nonzero line 225
  16. theorem OAI.InternalCatalan.fixedGaussianPlusRows_swaps line 229