I'm doing a mathematical formalization of Unique-Factorization Domains. But I can't find proper definitions.
I want to know how you call a non-zero non-unit element of a ring. Also I would like to have a precise definition of reducible element, and composite element, if these exists, preverably with references included.
Regards, Jens
Exactly that: "nonzero non-unit" (we can quibble about spacing and hyphens, though).
In some contexts, you might even be able to say just "nonzero" or "non-unit" because the other is clear by context. e.g., you ask the reader to "divide $a$ by non-unit $b$" (you probably don't want to divide by $0$, unless the domain you're working in has zero-divisors, so you dispense with "nonzero").
A reducible element is an element that is the product of two or more non-unit elements. For example, in $\mathbb{Z}$ we have $2 = -1 \times -2$, but $-1$ is a unit so that doesn't count and so $2$ is irreducible. Compare $-10 = -2 \times 5$, in which neither $-2$ nor $5$ is a unit.
If you're only concerned with UFD's, then you don't have to worry about the difference between irreducibles and primes, they're the same. In non-UFD's, that's not always the case.