Description: A right ideal is a left ideal of the opposite non-unital ring. This
theorem shows that this definition corresponds to the usual textbook
definition of a right ideal of a ring to be a subgroup of the additive
group of the ring which is closed under right-multiplication by elements
of the full ring. (Contributed by AV, 21-Mar-2025)