Prove2Me

lean_workbook_plus_82548

Proved

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

Lemma 2: AB=−BA→A3B=−BA3AB=-BA \rightarrow A^3B=-BA^3 and AB3=−B3AAB^3=-B^3A

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

View graph