Anne Baanen (Dec 05 2019 at 14:59):
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 (Dec 05 2019 at 15:02):
@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 (Dec 05 2019 at 15:06):
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 (Dec 05 2019 at 15:09):
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 (Dec 05 2019 at 15:13):
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.
Last updated: May 06 2021 at 19:30 UTC