mathlib

16e2c6ca - chore(data/matrix/basic): lemmas for `minor` about `diagonal`, `one`, and `mul` (#7133)

chore(data/matrix/basic): lemmas for `minor` about `diagonal`, `one`, and `mul` (#7133) The `minor_mul` lemma here has weaker hypotheses than the previous `reindex_mul`, as it only requires one mapping to be bijective.