Paper XII · Interactive proof

Try a proof in Lean

An idempotent in a commutative local ring is either zero or one. Explore Proposition 3.4, edit its proof, and see what Lean says.

A live editor, alongside the paper

Load the editor to check the proof automatically. Click a proof step to see its goal; open All Messages for diagnostics. The final #check displays the theorem’s type.

Powered by live.lean-lang.org. Loading connects to that service; code you enter is sent there for checking. An internet connection is required.

Open original proof in a new tab

Original source below. The live editor loads only when you choose it.

Original source · LocalIdempotents.lean

import Mathlib.RingTheory.LocalRing.Basic

/-! Paper XII, Proposition 3.4. -/
namespace PaperXII.LocalIdempotents

/-- Every idempotent in a commutative local ring is zero or one. -/
theorem eq_zero_or_one {R : Type*} [CommRing R] [IsLocalRing R]
    (e : R) (he : e * e = e) : e = 0 ∨ e = 1 := by
  rcases IsLocalRing.isUnit_or_isUnit_one_sub_self e with h | h
  · right
    exact h.mul_left_cancel (he.trans (mul_one e).symm)
  · left
    apply h.mul_left_cancel
    calc
      (1 - e) * e = 0 := by rw [sub_mul, one_mul, he, sub_self]
      _ = (1 - e) * 0 := (mul_zero _).symm

end PaperXII.LocalIdempotents

Source, Lean version, and scope

The starting proof is the complete retained LocalIdempotents.lean from Paper XII. The playground adds one #check command after the file; it does not alter the original download.

The editor uses the live service’s MathlibDemo project. Its Lean and Mathlib versions can change and are shown inside the editor. This is a live experiment on the service’s environment, rather than a reproduction of the paper’s pinned project.

This pilot checks one file. It does not replay the full paper, load the collection’s other project modules, or update recorded verification and coverage labels. Results and warnings are shown by Lean inside the editor; this page does not assign a proof-success badge.

Source checksum and playground record · Paper XII overview and evidence