Summary
- Added new statement for the ascending chain condition
- Removed unnecessary type restrictions for elementary matrix operations
- Renamed least_squares_solution -> least_squares_approximation
The file was modified | thys/Echelon_Form/Rings2.thy (diff) |
The file was modified | thys/Gauss_Jordan/Elementary_Operations.thy (diff) |
The file was modified | thys/QR_Decomposition/Least_Squares_Approximation.thy (diff) |