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)
:
Ring R
Equations
- non_unital_w_e_is_ring e is_left_unit is_right_unit = Ring.ofMinimalAxioms ⋯ ⋯ ⋯ ⋯ is_left_unit is_right_unit ⋯ ⋯