Documentation

ArtinWedderburn.NonUnitalToUnital

instance e_one {R : Type u_1} (e : R) :
One R
Equations
def non_unital_w_e_is_ring {R : Type u_1} [NonUnitalRing R] (e : R) (is_left_unit : ∀ (x : R), e * x = x) (is_right_unit : ∀ (x : R), x * e = x) :
Equations
Instances For