(Group action of) SL(n) in mathlib

Stream: maths

[Anne Baanen]

Hi! I want to take quotients modulo the action of SL(n) on some structure, but I can't find anything about SL(n) or matrix inverses in mathlib. Am I overlooking something, or is this missing from mathlib?

[Anne Baanen]

@Rob Lewis just said in person that it is indeed not formalized yet. Follow-up question: what would be the best way to define inverses?

[Anne Baanen]

Since mathlib typically defines partial operations by defining a total function and assuming the relevant preconditions in the theorems about this operation, my guess would be to start with pseudoinverses and then show that these are true inverses if the determinant is invertible, right?

[Chris Hughes]

I think there are a lot of different types of pseudoinverse. It would be desirable for the inverse function to return a left inverse if it exists and a right inverse if it exists for rectangular matrices.

[Anne Baanen]

The pseudoinverse I was thinking of is apparently called the Moore-Penrose inverse. IIRC, it is also the left or right inverse if only one of them exists.