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 via Ring.ofMinimalAxioms.

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.

Equations

• LeanPool.ArtinWedderburn.nonUnitalWEIsRing e is_left_unit is_right_unit = Ring.ofMinimalAxioms ⋯ ⋯ ⋯ ⋯ is_left_unit is_right_unit ⋯ ⋯