lean_workbook_plus_23891

Proved

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

Find the product of the matrices $T = \begin{pmatrix} 1 & 0 \\ 0 & 0 \end{pmatrix}$ and $U = \begin{pmatrix} 0 & 1 \\ 0 & 1 \end{pmatrix}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_23891 (T U : Matrix (Fin 2) (Fin 2) ℚ) (hT : T =![![1, 0],![0, 0]]) (hU : U =![![0, 1],![0, 1]]) : T * U =![![0, 1],![0, 0]]   :=  by sorry

Source

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

View graph