lean_workbook_plus_75396

Proved

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

Let $A \in \mathcal{M}_2 \left(\mathbb{Q}\right)$ , such that $\det(A^2-2I_2)=0$ . Prove that $A^2=2I_2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75396 {A : Matrix (Fin 2) (Fin 2) ℚ} (hA : A ^ 2 - 2 • (1 : Matrix (Fin 2) (Fin 2) ℚ) = 0) : A ^ 2 = 2 • (1 : Matrix (Fin 2) (Fin 2) ℚ)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph