Documentation

Mathlib.Algebra.Ring.Idempotents

Idempotents #

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

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 (x1 x2 : M) => x1 * x2] (a : M) :
    theorem IsIdempotentElem.eq {M : Type u_1} [Mul M] {p : M} (h : IsIdempotentElem p) :
    p * p = p
    theorem IsIdempotentElem.mul_of_commute {S : Type u_3} [Semigroup S] {p : S} {q : S} (h : Commute p q) (h₁ : IsIdempotentElem p) (h₂ : IsIdempotentElem q) :
    theorem IsIdempotentElem.mul {M : Type u_9} [CommSemigroup M] {e₁ : M} {e₂ : M} (he₁ : IsIdempotentElem e₁) (he₂ : IsIdempotentElem e₂) :
    IsIdempotentElem (e₁ * e₂)
    theorem IsIdempotentElem.pow {N : Type u_2} [Monoid N] {p : N} (n : ) (h : IsIdempotentElem p) :
    theorem IsIdempotentElem.pow_succ_eq {N : Type u_2} [Monoid N] {p : N} (n : ) (h : IsIdempotentElem p) :
    p ^ (n + 1) = p
    @[simp]
    theorem IsIdempotentElem.iff_eq_one {G : Type u_7} [Group G] {p : G} :
    @[simp]
    theorem IsIdempotentElem.iff_eq_zero_or_one {G₀ : Type u_8} [CancelMonoidWithZero G₀] {p : G₀} :
    theorem IsIdempotentElem.map {M : Type u_9} {N : Type u_10} {F : Type u_11} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] {e : M} (he : IsIdempotentElem e) (f : F) :

    Instances on Subtype IsIdempotentElem #

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