lean_workbook_plus_40624

Proved

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

$AB^2 - ABA = 0 \iff AB^2 = ABA$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_40624 (R : Type*) [CommRing R]
  (A B : Matrix (Fin 2) (Fin 2) R) :
  A * B ^ 2 - A * B * A = 0 ↔ A * B ^ 2 = A * B * A   :=  by sorry

Source

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

View graph