Add the Moore-Penrose pseudo-inverse

Note that the naive definition of

import Mathlib

variable {m n R : Type*} [CommRing R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]

noncomputable def pinv (A : Matrix m n R) : Matrix n m R :=
  (Aᵀ * A)⁻¹ * Aᵀ

only works when FIntype.card m >= Fintype.card n, and even then only when rank A = Fintype.card n.

Some possible references for a generalized definition:

• The generalized Moore-Penrose inverse, Mar 1992
• The Moore-Penrose inverse over a commutative ring, Dec 1992

A quick attempt at the second one seems to start with:

def IsMoorePenroseInverse {α β γ δ} [HMul α β γ] [HMul β α δ] [HMul γ α α] [HMul δ β β] [Star γ] [Star δ]
    (A : α) (As : β) :=
  A * As * A = A ∧ As * A * As = As ∧ star (A * As) = A * As ∧ star (As * A) = As * A

Zulip threads:

• #maths > (Group action of) SL(n) in mathlib @ 💬
• #new members > Dan Packer - Matrix Theory in Mathlib? @ 💬

Start with the issue's naive pinv definition and the proposed IsMoorePenroseInverse typeclass-style predicate, then read the linked papers and Zulip threads for the intended generalized definition. Done would require an agreed Moore–Penrose inverse design over the stated algebraic structures, together with its supporting mathlib definitions and theorems.