Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-19 21:51 e8ca35f1

View on Github →

chore(linear_algebra/matrix/block): remove the _matrix suffix from matrix.block_triangular_matrix (#16155) The same is done for the primed version. There's no need to have the word matrix in this definition twice.

Estimated changes