Left Noetherian domain Ore lemma (source code)

= Left Noetherian domain Ore lemma
{title2=$R\text{ left Noetherian domain}\implies R\setminus\{0\}\text{ left Ore}$}

In a <noncommutative domain> that is a <left Noetherian ring>, two nonzero principal <left ideals> always intersect nontrivially. If $Ra\cap Rb=0$, a relation $\sum_{i=0}^m u_iab^i=0$ first forces $u_0a\in Ra\cap Rb$, then $u_0=0$. Right cancellation of $b$ and repetition give all $u_i=0$. Hence $\sum_{i\geq0}Rab^i$ is an infinite <direct sum> of nonzero <left ideals>, whose finite partial sums violate the <ascending chain condition>. A nonzero member of $Rr\cap Rs$ supplies the equality $s'r=r's$ with $s'\ne0$, proving the <left Ore set> condition for all nonzero elements.