`BookProof.ChapterF4.pseudoInverse_left_inverse` {k m : ℕ} (Φ : Matrix (Fin k) (Fin m) ℝ) [Invertible (Φᵀ * Φ)] : ⅟(Φᵀ * Φ) * Φᵀ * Φ = 1

Initializing...

`BookProof.ChapterF4.pseudoInverse_left_inverse` {k m : ℕ} (Φ : Matrix (Fin k) (Fin m) ℝ) [Invertible (Φᵀ * Φ)] : ⅟(Φᵀ * Φ) * Φᵀ * Φ = 1 · Prove2Me