`BookProof.ChapterF4.pseudoinverse_left_inverse` {m n : ℕ} (Φ : Matrix (Fin m) (Fin n) ℂ) (h : IsUnit (Φᴴ * Φ).det) : ((Φᴴ * Φ)⁻¹ * Φᴴ) * Φ = 1

Initializing...

`BookProof.ChapterF4.pseudoinverse_left_inverse` {m n : ℕ} (Φ : Matrix (Fin m) (Fin n) ℂ) (h : IsUnit (Φᴴ * Φ).det) : ((Φᴴ * Φ)⁻¹ * Φᴴ) * Φ = 1 · Prove2Me