[Merged by Bors] - feat(linear_algebra/matrix/transvection): matrices are generated by transvections and diagonal matrices

[sgouezel]

One version of Gauss' pivot: any matrix can be obtained starting from a diagonal matrix and doing elementary moves on rows and columns. Phrased in terms of multiplication by transvections.

---

• depends on: [Merged by Bors] - refactor(data/matrix): put std_basis_matrix in its own file #9088

[semorrison]

I am hesitant to complain about this, but I think in English speaking mathematics we consistently use the phrase "elementary matrix" rather than "transvection".

(Unfortunately on wikipedia the interlanguage link from the French "transvection" points to the English "shear matrix", which is not correct, being more general.)

[semorrison]

This is really lovely, and I'm so pleased this is coming to mathlib! This has been an elementary (ha!) hole for a long time.

Certainly not for this PR, but someday someone may like to generalise this argument to work over a PID, where instead of elementary matrices you need invertible 2x2 matrices. This can give you a formulation of Smith normal form, and indeed one could deduce today's result from that one "just" by a lemma about writing 2x2 invertible matrices as products of elementary matrices (over a field). Unfortunately the induction is trickier here, as it involves an ideal as well as the size of the matrix.

[sgouezel]

I am hesitant to complain about this, but I think in English speaking mathematics we consistently use the phrase "elementary matrix" rather than "transvection".

(Unfortunately on wikipedia the interlanguage link from the French "transvection" points to the English "shear matrix", which is not correct, being more general.)

I am open to any suggestion from someone who knows the proper English wording. My problem with "elementary matrix" is that we already have this, for the matrix E i j with 1 at position (i, j) and 0 elsewhere (as opposed to transvections which, additionally, haves ones on the diagonal). Tell we how you want to phrase things, and I'll make the change!

[sgouezel]

I have added a sentence on the relationship with elementary matrices. Also moved all the material about E to matrix.basis and reexpressed it in terms of std_basis_matrix. And used the naming convention of pi.single everywhere.

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - refactor(data/matrix): put std_basis_matrix in its own file #9088

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

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