Documentation

Mathlib.Algebra.GroupWithZero.Idempotent

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
    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