Promoting a non-unital ring with a unit element to a unital ring

If a non-unital ring R has an element e that is both a left and a right identity, then R admits a (unital) ring structure with 1 = e.

@[reducible]

def LeanPool.ArtinWedderburn.eOne {R : Type u_1} (e : R) : One R

Designate e as the 1 element when building a unital Ring structure on R.

Equations

• LeanPool.ArtinWedderburn.eOne e = { one := e }

@[reducible]

def LeanPool.ArtinWedderburn.nonUnitalWEIsRing {R : Type u_1} [NonUnitalRing R] (e : R) (is_left_unit : ∀ (x : R), e * x = x) (is_right_unit : ∀ (x : R), x * e = x) : Ring R

Promote a non-unital ring R with a two-sided identity e to a unital Ring R.

The additive structure is inherited verbatim from the NonUnitalRing R instance, so the AddCommMonoid R carried by the result is the one already in scope; rebuilding it (as Ring.ofMinimalAxioms would) yields nsmulRec/zsmulRec instead and makes the two incomparable during instance synthesis.

Equations

• One or more equations did not get rendered due to their size.