# Idempotent elements of a group with zero #

source
theorem IsIdempotentElem.zero {M₀ : Type u_4} [MulZeroClass M₀] :
IsIdempotentElem 0
source
instance IsIdempotentElem.instZeroSubtype {M₀ : Type u_4} [MulZeroClass M₀] :
Zero { p : M₀ // IsIdempotentElem p }
Equations

- IsIdempotentElem.instZeroSubtype = { zero := ⟨0, ⋯⟩ }

source
@[simp]
theorem IsIdempotentElem.coe_zero {M₀ : Type u_4} [MulZeroClass M₀] :
↑0 = 0
source
@[simp]
theorem IsIdempotentElem.iff_eq_zero_or_one {G₀ : Type u_8} [CancelMonoidWithZero G₀] {p : G₀} :
IsIdempotentElem p ↔ p = 0 ∨ p = 1