lean_workbook_plus_4482

Proved

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

Let $A=B=\begin{bmatrix}1&1\\0&0\end{bmatrix}.$ Clearly $AB=BA=A^2=A.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4482 (A B : Matrix (Fin 2) (Fin 2) ℚ) (hA : A =![![1, 1],![0, 0]]) (hB : B =![![1, 1],![0, 0]]) : A * B = B * A ∧ A * B = A^2 ∧ A * B = A   :=  by sorry

Source

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

View graph