Commit 2021-04-12 12:44 16e2c6ca
View on Github →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.