mathlib
mathlib copied to clipboard
feat(linear_algebra/matrix): triangular matrices
This PR defines triangular matrices based on block-triangular matrices.
- [x] depends on: #14035
- [x] depends on: #16150
This PR/issue depends on:
- ~~leanprover-community/mathlib#14035~~
- ~~leanprover-community/mathlib#16150~~ By Dependent Issues (🤖). Happy coding!
Please add the awaiting-review label once CI is fixed (or if you need help).
Essentially all of the contents of this pull request have already been added independently now.