mathlib

447a2d6c - chore(data/matrix/basic): move numeral section into diagonal (#3022)

chore(data/matrix/basic): move numeral section into diagonal (#3022) Since the numeral section defines numerals for matrices as scalar multiples of `one_val`, which is the identity matrix, these are defined solely for diagonal matrices of type `matrix n n r`. So the numeral section should be in the diagonal section. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>