mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

feat(linear_algebra/matrix): triangular matrices

Open abentkamp opened this issue 3 years ago • 1 comments

This PR defines triangular matrices based on block-triangular matrices.

  • [x] depends on: #14035
  • [x] depends on: #16150

Open in Gitpod

abentkamp avatar Aug 19 '22 10:08 abentkamp

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).

kim-em avatar Mar 29 '23 23:03 kim-em

Essentially all of the contents of this pull request have already been added independently now.

abentkamp avatar May 17 '23 10:05 abentkamp