Prove2Me

lean_workbook_plus_62132

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Use row reduction to find the inverse of the matrix: [9/27/2−7/2−5/2]\begin{bmatrix} 9/2 & 7/2 \\ -7/2 & -5/2 \end{bmatrix}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_62132 (A : Matrix (Fin 2) (Fin 2) ℚ) (hA : A =!![9 / 2, 7 / 2; -7 / 2, -5 / 2]) : A *!![-5 / 2, -7 / 2; 7 / 2, 9 / 2] = 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph