lean_workbook_plus_38236

Proved

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

Let A is associative ring in which $\forall a\in A$ $a^2=0$ and $\forall n\in\mathbb N$ $na=0\Rightarrow a=0.$ Prove that $abc=0,$ where $a\in A,$ $b\in A,$ $c\in A.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_38236 (A : Type*) [Ring A] (hA : ∀ a : A, a ^ 2 = 0) (hA' : ∀ n : ℕ, ∀ a : A, n * a = 0 → a = 0) (a b c : A) : a * b * c = 0   :=  by sorry

Source

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

View graph