The work to define gaussian elimination, a definition which in and of itself has no holes, so that all properties that had to be expressed were defined / given implementations.
Creates the module ZZGaussianElimination at ZZGaussianElimination.idr
Creates the expression gaussElimlz : (xs : Matrix n m ZZ) -> (gexs : Matrix n' m ZZ ** (spanslz gexs xs,rowEchelon gexs)), which to give any implementation to is considered implementing gaussian elimination in an extended sense.
Creates the module FinOrdering at FinOrdering.idr
Reintroduces decidable orderings, in FinOrdering, for Nat in this case.
The work to define gaussian elimination, a definition which in and of itself has no holes, so that all properties that had to be expressed were defined / given implementations.
gaussElimlz : (xs : Matrix n m ZZ) -> (gexs : Matrix n' m ZZ ** (spanslz gexs xs,rowEchelon gexs)), which to give any implementation to is considered implementing gaussian elimination in an extended sense.Natin this case.