Idempotent elements of a group with zero

theorem IsIdempotentElem.zero {M₀ : Type u_1} [MulZeroClass M₀] : IsIdempotentElem 0

@[instance_reducible]

instance IsIdempotentElem.instZeroSubtype {M₀ : Type u_1} [MulZeroClass M₀] : Zero { p : M₀ // IsIdempotentElem p }

Equations

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

@[simp]

theorem IsIdempotentElem.coe_zero {M₀ : Type u_1} [MulZeroClass M₀] : ↑0 = 0

@[simp]

theorem IsIdempotentElem.iff_eq_zero_or_one {G₀ : Type u_2} [MonoidWithZero G₀] [IsLeftCancelMulZero G₀] {p : G₀} : IsIdempotentElem p ↔ p = 0 ∨ p = 1

theorem IsIdempotentElem.eq_zero_or_one {G₀ : Type u_2} [MonoidWithZero G₀] [IsLeftCancelMulZero G₀] {p : G₀} : IsIdempotentElem p → p = 0 ∨ p = 1

Alias of the forward direction of IsIdempotentElem.iff_eq_zero_or_one.