matrix.minor wrong terminology?

Stream: maths

[Alexander Bentkamp]

I think the term "minor" is used in the wrong way in mathlib. Minors are the determinants of submatrices, not the submatrix itself. Should I make a PR to rename matrix.minor to matrix.submatrix?

[Moritz Doll]

technically it is not even a submatrix, right? you could have rows/columns that you reindex twice (i.e., the maps are not injective)

[Eric Wieser]

I think probably we don't need to worry about that though; we frequently use names that only actually match convention under extra assumptions

[Eric Wieser]

Such as module which isn't really a module without ring

[Eric Wieser]

Or monoid_hom which isn't really a monoid homomorphism without monoid

[Eric Wieser]

It's unfortunate that submatrix is almost twice as long a name

[Eric Wieser]

Note that on square matrices, matrix.minor A f f is the same as matrix.of (A on f) (docs#function.on_fun). Perhaps then simply matrix.on is a reasonable (protected) name?

[Johan Commelin]

I like matrix.on.

[Alexander Bentkamp]

#16063

[Yaël Dillies]

That will conflict with #14035.

[Alexander Bentkamp]

That's ok. When the first one gets merged, I am happy to update the other.

[Alexander Bentkamp]

The PR for on is ready, but @Anne Baanen and I aren't really happy about on. For me, it's because on is not really illuminating for newcomers. Indeed, submatrix is a bit long, but maybe acceptable? How about abbreviating it as submat or submx? Any other ideas?

[Eric Wieser]

/poll What should matrix.minor be called?

• matrix.minor
• matrix.on
• matrix.submat
• matrix.submx

[Eric Wieser]

Another similar definition is docs#finsupp.comap_domain, which does the same type of composition on the left; thought the name IMO would be worse here.

[Moritz Doll]

yet another similar definition is docs#linear_map.compl₁₂

[Anne Baanen]

Some other options I considered are to call this matrix.reindex and rename reindex to reindex_equiv, or matrix.(co)map_index.

[Eric Wieser]

That's made a little messy by the fact that src#matrix.reindex is implemented as reindex e f = minor e.symm f.symm; the direction is flipped, so one is not just a bundled version of the other

[Alexander Bentkamp]

Ok, submatrix seems to be the most popular. Here is the PR for submatrix: #16101

[Alexander Bentkamp]

merged!