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
@[implicit_reducible]
instance IsIdempotentElem.instZeroSubtype {M₀ : Type u_1} [MulZeroClass M₀] :
Zero { p : M₀ // IsIdempotentElem p }
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