Idempotents of a local ring

A local ring has no idempotents besides 0 and 1: splitting 1 = a + (1 - a) makes one of the two summands a unit, and an idempotent unit is 1.

theorem QuotientSubmoduleEquidistribution.Foundation.IsLocalRing.eq_zero_or_eq_one_of_isIdempotentElem {R : Type u_1} [Ring R] [IsLocalRing R] {a : R} (ha : IsIdempotentElem a) : a = 0 ∨ a = 1

An idempotent of a local ring is 0 or 1. Mathlib's IsLocalRing.isUnit_or_isUnit_one_sub_self is stated over a commutative ring, so the splitting of 1 = a + (1 - a) is taken here from IsLocalRing.isUnit_or_isUnit_of_isUnit_add, which holds over any semiring.