Theorems · Definition · ring theory

AlgEquiv.prodQuotientOfIsIdempotentElem

(R : Type u_1) →
  [inst : CommRing R] →
    {S : Type u_4} →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {e f : S} →
            IsIdempotentElem e →
              IsIdempotentElem f → e + f = 1 → e * f = 0 → S ≃ₐ[R] (S ⧸ Ideal.span {e}) × S ⧸ Ideal.span {f}

If e and f are idempotent elements such that e + f = 1 and e * f = 0, S is isomorphic as an R-algebra to S ⧸ (e) × S ⧸ (f).

Defined in

Mathlib.RingTheory.Idempotents

Cited by

5 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebra