# Idempotents #

This file defines idempotents for an arbitrary multiplication and proves some basic results, including:

• IsIdempotentElem.mul_of_commute: In a semigroup, the product of two commuting idempotents is an idempotent;
• IsIdempotentElem.one_sub_iff: In a (non-associative) ring, p is an idempotent if and only if 1-p is an idempotent.
• IsIdempotentElem.pow_succ_eq: In a monoid p ^ (n+1) = p for p an idempotent and n a natural number.

## Tags #

projection, idempotent

def IsIdempotentElem {M : Type u_1} [Mul M] (p : M) :

An element p is said to be idempotent if p * p = p

Equations
Instances For
theorem IsIdempotentElem.of_isIdempotent {M : Type u_1} [Mul M] [Std.IdempotentOp fun (x x_1 : M) => x * x_1] (a : M) :
theorem IsIdempotentElem.eq {M : Type u_1} [Mul M] {p : M} (h : ) :
p * p = p
theorem IsIdempotentElem.mul_of_commute {S : Type u_3} [] {p : S} {q : S} (h : Commute p q) (h₁ : ) (h₂ : ) :
theorem IsIdempotentElem.zero {M₀ : Type u_4} [] :
theorem IsIdempotentElem.one {M₁ : Type u_5} [] :
theorem IsIdempotentElem.one_sub {R : Type u_6} [] {p : R} (h : ) :
@[simp]
theorem IsIdempotentElem.one_sub_iff {R : Type u_6} [] {p : R} :
theorem IsIdempotentElem.pow {N : Type u_2} [] {p : N} (n : ) (h : ) :
theorem IsIdempotentElem.pow_succ_eq {N : Type u_2} [] {p : N} (n : ) (h : ) :
p ^ (n + 1) = p
@[simp]
theorem IsIdempotentElem.iff_eq_one {G : Type u_7} [] {p : G} :
p = 1
@[simp]
theorem IsIdempotentElem.iff_eq_zero_or_one {G₀ : Type u_8} [] {p : G₀} :
p = 0 p = 1

### Instances on Subtype IsIdempotentElem#

instance IsIdempotentElem.instZeroSubtype {M₀ : Type u_4} [] :
Zero { p : M₀ // }
Equations
• IsIdempotentElem.instZeroSubtype = { zero := 0, }
@[simp]
theorem IsIdempotentElem.coe_zero {M₀ : Type u_4} [] :
0 = 0
instance IsIdempotentElem.instOneSubtype {M₁ : Type u_5} [] :
One { p : M₁ // }
Equations
• IsIdempotentElem.instOneSubtype = { one := 1, }
@[simp]
theorem IsIdempotentElem.coe_one {M₁ : Type u_5} [] :
1 = 1
instance IsIdempotentElem.instHasComplSubtype {R : Type u_6} [] :
HasCompl { p : R // }
Equations
• IsIdempotentElem.instHasComplSubtype = { compl := fun (p : { p : R // }) => 1 - p, }
@[simp]
theorem IsIdempotentElem.coe_compl {R : Type u_6} [] (p : { p : R // }) :
p = 1 - p
@[simp]
theorem IsIdempotentElem.compl_compl {R : Type u_6} [] (p : { p : R // }) :
@[simp]
theorem IsIdempotentElem.zero_compl {R : Type u_6} [] :
0 = 1
@[simp]
theorem IsIdempotentElem.one_compl {R : Type u_6} [] :
1 = 0