Upper triangular matrix and Strictly upper triangular matrix

Stream: Is there code for X?

[Edison Xie]

I understand that our convention of writing some matrix M to be IsUpperTriangular is to write M.BlockTriangular id, but what do I do if I want a strictly upper triangular matrix?
This came up when I'm looking for Engel's theorem in Mathlib, I've found LieAlgebra.isNilpotent_iff_forall which gives one version of it (i.e ad x being nilpotent for all x), but I couldn't find the version about every element can be represented by a strictly upper triangular matrix (also we just don't have Lie's theoem), is there anyone working on this?

[Edison Xie]

Also do we want names (possibly abbrevs) for upper and strictly upper triangular matrices or the way we do it now is good enough?