lean_workbook_plus_47445

Proved

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

Given matrices $A: =\left(\begin{matrix}1&1\\0&0\end{matrix}\right)$ and $B: =\left(\begin{matrix}0&0\\1&1\end{matrix}\right)$ , show that they satisfy $A^2=AB=A$ and $B^2=BA=B$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source

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

View graph