mathlib3

2f38ccb4 - chore(data/matrix/basic): add lemmas about powers of matrices (#13815)

chore(data/matrix/basic): add lemmas about powers of matrices (#13815) Shows that: * natural powers commute with `transpose`, `conj_transpose`, `diagonal`, `block_diagonal`, and `block_diagonal'`. * integer powers commute with `transpose`, and `conj_transpose`.