mathlib
e8ca35f1
- chore(linear_algebra/matrix/block): remove the `_matrix` suffix from `matrix.block_triangular_matrix` (#16155)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
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.
Author
eric-wieser
Parents
faed3a7f
Loading