Documentation

Mathlib.Algebra.Ring.Idempotents

Idempotents #

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

Tags #

projection, idempotent

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

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

Equations
theorem IsIdempotentElem.of_isIdempotent {M : Type u_1} [inst : Mul M] [inst : IsIdempotent M fun x x_1 => x * x_1] (a : M) :
theorem IsIdempotentElem.eq {M : Type u_1} [inst : Mul M] {p : M} (h : IsIdempotentElem p) :
p * p = p
theorem IsIdempotentElem.mul_of_commute {S : Type u_1} [inst : Semigroup S] {p : S} {q : S} (h : Commute p q) (h₁ : IsIdempotentElem p) (h₂ : IsIdempotentElem q) :
theorem IsIdempotentElem.one {M₁ : Type u_1} [inst : MulOneClass M₁] :
theorem IsIdempotentElem.one_sub {R : Type u_1} [inst : NonAssocRing R] {p : R} (h : IsIdempotentElem p) :
@[simp]
theorem IsIdempotentElem.pow {N : Type u_1} [inst : Monoid N] {p : N} (n : ) (h : IsIdempotentElem p) :
theorem IsIdempotentElem.pow_succ_eq {N : Type u_1} [inst : Monoid N] {p : N} (n : ) (h : IsIdempotentElem p) :
p ^ (n + 1) = p
@[simp]
theorem IsIdempotentElem.iff_eq_one {G : Type u_1} [inst : Group G] {p : G} :
@[simp]
theorem IsIdempotentElem.iff_eq_zero_or_one {G₀ : Type u_1} [inst : CancelMonoidWithZero G₀] {p : G₀} :

Instances on Subtype IsIdempotentElem #

Equations
  • IsIdempotentElem.instZeroSubtypeIsIdempotentElemToMul = { zero := { val := 0, property := (_ : IsIdempotentElem 0) } }
@[simp]
theorem IsIdempotentElem.coe_zero {M₀ : Type u_1} [inst : MulZeroClass M₀] :
0 = 0
Equations
  • IsIdempotentElem.instOneSubtypeIsIdempotentElemToMul = { one := { val := 1, property := (_ : IsIdempotentElem 1) } }
@[simp]
theorem IsIdempotentElem.coe_one {M₁ : Type u_1} [inst : MulOneClass M₁] :
1 = 1
Equations
  • IsIdempotentElem.instHasComplSubtypeIsIdempotentElemToMulToNonUnitalNonAssocRing = { compl := fun p => { val := 1 - p, property := (_ : IsIdempotentElem (1 - p)) } }
@[simp]
theorem IsIdempotentElem.coe_compl {R : Type u_1} [inst : NonAssocRing R] (p : { p // IsIdempotentElem p }) :
↑(p) = 1 - p
@[simp]
theorem IsIdempotentElem.compl_compl {R : Type u_1} [inst : NonAssocRing R] (p : { p // IsIdempotentElem p }) :
@[simp]
theorem IsIdempotentElem.zero_compl {R : Type u_1} [inst : NonAssocRing R] :
0 = 1
@[simp]
theorem IsIdempotentElem.one_compl {R : Type u_1} [inst : NonAssocRing R] :
1 = 0