lean_workbook_plus_60484

Proved

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

Take $A=\begin{pmatrix}1&0\\0&0\end{pmatrix},B=\begin{pmatrix}0&0\\0&1\end{pmatrix}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source

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

View graph