Prove2Me

lean_workbook_plus_13241

Proved

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

Lemma 5: AB=−BA→A3B3=−B3A3AB=-BA \rightarrow A^3B^3=-B^3A^3

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_13241 (R : Type*) [Ring R] (A B : Matrix (Fin 2) (Fin 2) R) (h : A * B = -(B * A)) : A ^ 3 * B ^ 3 = -(B ^ 3 * A ^ 3)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph