mathlib
55e2dfde - chore(data.matrix): rename `minor` to `submatrix` (#16101)

Commit
3 years ago
chore(data.matrix): rename `minor` to `submatrix` (#16101) As discussed on Zulip: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/matrix.2Eminor.20wrong.20terminology.3F This is an alternative to the previous plan to rename `minor` to `on` in #16063. Moreover, I have adapted some documentation in `src/linear_algebra/matrix/adjugate.lean` that also used the term "minor" in the wrong way.
Author
Parents
Loading