mathlib3
54ac48ad - chore(data/matrix/basic): add simp lemmas about `minor`, move `reindex` to `matrix.basic` since it knows nothing about linear algebra (#7083)

Commit
4 years ago
chore(data/matrix/basic): add simp lemmas about `minor`, move `reindex` to `matrix.basic` since it knows nothing about linear algebra (#7083)
Author
Parents
Loading