lean_workbook_plus_38120

Proved

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

Yes (and it's true over any field): \n\n $\begin{pmatrix}I&0\\B&I\end{pmatrix} \begin{pmatrix}AB-I&A\\0&-I\end{pmatrix} \begin{pmatrix}I&0\\-B&I\end{pmatrix} = \begin{pmatrix}-I&A\\0&BA-I\end{pmatrix}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_38120 (R : Type*) [Field R] (A B : Matrix (Fin 2) (Fin 2) R) : 
 !![1, 0; B, 1] *!![A * B - 1, A; 0, -1] *!![1, 0; -B, 1] =!![-1, A; 0, B * A - 1]   :=  by sorry

Source

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

View graph