Idempotent integers in a ring of characteristic zero

In a ring of characteristic zero the integers embed injectively, so an integer is idempotent in the ring exactly when it is idempotent in ℤ, that is, when it is 0 or 1. Consequently an idempotent other than 0 and 1 is not an integer.

Main results

• TauCeti.isIdempotentElem_intCast_iff: the cast of n : ℤ is idempotent exactly when n is 0 or 1.

@[simp]

theorem TauCeti.isIdempotentElem_intCast_iff {R : Type u_1} [NonAssocRing R] [CharZero R] {n : ℤ} : IsIdempotentElem ↑n ↔ n = 0 ∨ n = 1

In a ring of characteristic zero, the cast of an integer n is idempotent exactly when n is 0 or 1.