[Merged by Bors] - feat(linear_algebra/matrix/reindex): add some lemmas

[faenuccio]

From LTE
Added lemmas reindex_linear_equiv_trans, reindex_linear_equiv_comp, reindex_linear_equiv_comp_apply, reindex_linear_equiv_one and mul_reindex_linear_equiv_mul_one needed in LTE.

---

[Vierkantor]

A few stylistic suggestions:

[faenuccio]

Perhaps the thing to do is either:

• Add a copy of every lemma about minor for reindex
• Edit the docstring of reindex to point users to reindex_apply, and state that all the interesting lemmas are stated about minor

For the time being, it does not seems to me that the linter is complaining. As an aside, it is complaining a lot about a line which is more than 100 characters long, but it does not seem to me to point to the line: I see

+ find src archive counterexamples -name '*.lean'
+ xargs ./scripts/lint-style.py
Error: ERR_LIN: Line has more than 100 characters
Error: Process completed with exit code 123.

but can't understand what to fix. That being said, I have two problems with minor:

• AFAIK, a minor is a determinant, whereas in mathlib they are submatrices. Why is it so?
• reindexing and taking minors seem to be different operations mathematically, although the way they are implemented in mathlib makes them look analogous.

[faenuccio]

I have at any rate wiped off the reindex_one, as the minor could close the goal I was interested in, in linear_algebra/matrix/reindex.lean.

[Vierkantor]

For the time being, it does not seems to me that the linter is complaining. As an aside, it is complaining a lot about a line which is more than 100 characters long, but it does not seem to me to point to the line: I see

+ find src archive counterexamples -name '*.lean'
+ xargs ./scripts/lint-style.py
Error: ERR_LIN: Line has more than 100 characters
Error: Process completed with exit code 123.

but can't understand what to fix.

You can see style errors in the "changes" tab of the PR - GitHub tries to be smart and parse out the data, hiding it in the process. I already added a suggestion to fix the long line, so don't worry about this anymore.

* AFAIK, a `minor` is a determinant, whereas in `mathlib` they are submatrices. Why is it so?

I also know minor as a determinant of a submatrix, and my textbooks and Wikipedia agree. It seems the name wasn't remarked on when they were introduced in #389 and now we're stuck with an uncommon (or even confusing/inaccurate?) name.

* reindexing and taking minors seem to be different operations mathematically, although the way they are implemented in `mathlib` makes them look analogous.

The trick is that M.minor row col is not "really" a submatrix, since row and col don't have to be injective! So it's more like "map the index" rather than taking a submatrix per se.

[faenuccio]

Ok, all in all I am a bit confused. What should I do to get the PR through? If I understand correctly, @eric-wieser was suggesting that instead of adding this lemma, one uses the basic version about reindex in data\matrix. It could be a good idea, and if this is what is required I can try to see if in the LTE each time they occur we can make do with this trick. But are they really painful? Or am I overlooking something?

[Vierkantor]

Ok, all in all I am a bit confused. What should I do to get the PR through? If I understand correctly, @eric-wieser was suggesting that instead of adding this lemma, one uses the basic version about reindex in data\matrix.

I understand the remarks as referring to the following two guidelines:

If the proof of your lemma is simply by simp, then tagging it @[simp] is often a bad idea: you don't gain anything since simp can already prove the result, and grouping together the wrong things in simp might(?) cause it to get stuck.

There's another guideline that says: if you add a lemma where simp can already do something on the conclusion, you probably want to restate that lemma (either additionally or in the place of the original) on the output of simp instead. For example, simp turns reindex_linear_equiv e M into M.minor e e, so a lemma like reindex_linear_equiv e 1 = 1 should be restated as minor 1 e e = 1. Only the latter should be tagged @[simp], following the previous guidelines.

The result for the reindex_linear_equiv lemmas you added is to (also) add them for matrix.minor, which luckily already exist so you don't need to do much.

[Vierkantor]

Looks good to me, thanks for perservering! I'll let @eric-wieser make the final decision.

[eric-wieser]

Thanks for the persistence!

bors d+

[eric-wieser]

May as well use the notation:

Suggested change

	((1 : matrix o o α).minor e₁ e₂).mul M = minor M (e₂.symm ∘ e₁) id :=
	(1 : matrix o o α).minor e₁ e₂ ⬝ M = minor M (e₂.symm ∘ e₁) id :=

[bors]

✌️ faenuccio can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[faenuccio]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests