Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-11 18:53 447a2d6c

View on Github →

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.

Estimated changes