Documentation

Mathlib.Algebra.GroupWithZero.Idempotent

Idempotent elements of a group with zero #

source
📐 coverage
theorem IsIdempotentElem.zero {M₀ : Type u_1} [MulZeroClass M₀] :
IsIdempotentElem 0
source
🔸 coverage
instance IsIdempotentElem.instZeroSubtype {M₀ : Type u_1} [MulZeroClass M₀] :
Zero { p : M₀ // IsIdempotentElem p }
Equations
    source
    📐 coverage
    @[simp]
    theorem IsIdempotentElem.coe_zero {M₀ : Type u_1} [MulZeroClass M₀] :
    ↑0 = 0
    source
    📐 coverage
    @[simp]
    theorem IsIdempotentElem.iff_eq_zero_or_one {G₀ : Type u_2} [MonoidWithZero G₀] [IsLeftCancelMulZero G₀] {p : G₀} :
    IsIdempotentElem p ↔ p = 0 ∨ p = 1