Paper XII · Lean source

LocalIdempotents.lean

Inherited / related evidence Coverage and evidence

The edition relies on earlier or related formal evidence. That evidence is not a fresh full-edition replay.

This viewer reads the retained source; it does not run Lean or assign new claim mappings.

PaperXII/LocalIdempotents.lean18 lines

Original source path

core/publication/source/lean_guide/formal_release/lean/PaperXII/LocalIdempotents.lean

1 import Mathlib.RingTheory.LocalRing.Basic
2 
3 /-! Paper XII, Proposition 3.4. -/
4 namespace PaperXII.LocalIdempotents
5 
6 /-- Every idempotent in a commutative local ring is zero or one. -/
7 theorem eq_zero_or_one {R : Type*} [CommRing R] [IsLocalRing R]
8     (e : R) (he : e * e = e) : e = 0 ∨ e = 1 := by
9   rcases IsLocalRing.isUnit_or_isUnit_one_sub_self e with h | h
10   · right
11     exact h.mul_left_cancel (he.trans (mul_one e).symm)
12   · left
13     apply h.mul_left_cancel
14     calc
15       (1 - e) * e = 0 := by rw [sub_mul, one_mul, he, sub_self]
16       _ = (1 - e) * 0 := (mul_zero _).symm
17 
18 end PaperXII.LocalIdempotents

Back to source controls

Original file and source record

This copy matches the recorded source file. Its publication here does not change the work’s review status.

SHA-256: e34c194a98e51680b23542d6a74ed35abcde3f6c50136616ae0d01ef64e130db

Original source on GitHub

Back to Paper XII: Patching Support, Hecke Packets, and Conditional Automorphic Completion