lean_workbook_plus_38372

Proved

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

Let $(A,+,\cdot)$ a ring with the following property: $x^2=x$ for any $x\in A$ . Show that $x+x=0$ for any $x\in A$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_38372 (A : Type*) [Ring A] (h : ∀ x : A, x ^ 2 = x) : ∀ x : A, x + x = 0   :=  by sorry

Source