I'm looking for a reference to the following corollary, which comes as a by-product of a more general result.

> **Corollary.** Let $R$ be a [non-trivial][1] Dedekind-finite unital ring (either commutative or not), and let $k \in \mathbf N^+$. Then the [monoid ring][2] $R[\mathbb N^k]$ has infinitely many pairwise non-associate irreducible elements.

*Notes.* (i) A unital ring is called *Dedekind-finite* provided that $xy = 1_R$ for some $x, y \in R$ only if $yx = 1_R$. (ii) $\mathbb N^k$ is the monoid $(\mathbf N^k, +)$. So in particular, if $R$ is commutative, then $R[\mathbb N^k]$ is a ring of polynomials in $k$ variables with coefficients in $R$.


  [1]: https://en.wikipedia.org/wiki/Zero_ring
  [2]: https://en.wikipedia.org/wiki/Monoid_ring