Theorems · Definition · ring theory

CompleteOrthogonalIdempotents.ringEquivOfIsMulCentral

{R : Type u_1} →
  {I : Type u_2} →
    [inst : Fintype I] →
      {e : I → R} →
        [inst_1 : Semiring R] →
          (he : CompleteOrthogonalIdempotents e) → (∀ (i : I), IsMulCentral (e i)) → R ≃+* ((i : I) → ⋯.Corner)

A complete orthogonal family of central idempotents in a semiring give rise to a direct product decomposition.

Defined in

Mathlib.RingTheory.Idempotents

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeSemiring