Formalizing $na$ for $n\in\mathbb{Z}$ and $a\in R$ where $R$ is a ring.

Question

Let $R$ be a ring and let $n\in\mathbb{Z}$.

Given $a\in R$, I've seen $na$ defined as $$ na:=\begin{cases}0&\text{if }n=0,\\\underbrace{a+a+\cdots+a}_{n\text{ times}}&\text{if }n>0,\\\underbrace{-a-a-\cdots-a}_{|n|\text{ times}}&\text{if }n<0.\end{cases}\tag{1} $$ With this definition, I've even read that $$ (m+n)a=ma+na\tag{2} $$ and $$ (mn)1=(m1)(n1)\tag{3} $$ are obvious (and I do agree with this view).

Question:

(i) Isn't $(1)$ informal? If so, would $na$ be formally defined, for $n\geq0$, recursively via the equations \begin{align*} 0a&=0\tag{4}\\ (n+1)a&=na+a\tag{5} \end{align*} and for $n<0$ by $na:=-(-n)a$ ?

(ii) Would formal proofs of $(2)$ and $(3)$ be as given below?

I'm asking since I've never seen this done...

Proof of $(2)$: For fixed $m$, proceed by induction on $n$ for $n\geq-m$. Then, for $n<-m$, $$ (m+n)a=-(-m-n)a=-((-m)a+(-n)a)=-(-m)a-(-n)a=ma+na $$

Proof of $(3)$: First show the result for $n\in\mathbb{Z}$ and $m\geq0$. To do so, prove by induction on $m$ for fixed $n$ that $(mn)1=m(n1)$ (making use of $(2)$) and then that this equals $(m1)(n1)$, by induction on $m$ again. Finally, for $m<0$, $$ (mn)1=(-(-m)n)1=-((-m)n)1=-((-m)1)(n1)=(-(-m)1)(n1)=(m1)(n1) $$

Answer 1

Your comment in the answer to @lhf is correct. This is formalized in set theory with the concept of recursive definition, in this case, the recursive definition of a homomorphism $f_a : \mathbb{Z} \to R$ with the property that $f_a(1)=a$.

Informally it goes just like what you wrote: first define $f_a(1)$ which has already been done; then define $f_a(n)$ by a formula expressed in terms of the values of $f_a(1),…,f_a(n-1)$, in this case $f_a(n)=f_a(n-1)+a$. The principal of recursive definition then guarantees the existence of this function $f_a$ on the natural numbers, and then you extend to zero and negative numbers in the obvious way.

This informal way of doing a recursive definition is almost universally acceptable, because a complete and formal recursive definition is often quite tedious and without much mathematical interest. There are definitely exceptions, though, where one really ought to write out the details of a recursive definition.

Once you've proved the existence of $f_a$, you still want to prove that it is a homomorphism, and this will be a proof by induction.

And as long as we've gone this far, you may also wish to formally verify, using the axioms of set theory, that the formula $a \mapsto f_a$ defines a function from $R$ to the set of homomorphisms $\mathbb{Z} \to R$. This way one can completely formalize the definition of $n \cdot a$ to be $n \cdot a = f_a(n)$.

Answer 2

$na$ is simply $a^n$ in the additive group of $R$, written additively of course.

In other words, since $\mathbb Z$ is a cyclic group generated by $1 \in \mathbb Z$, there is a unique homomorphism $\mu: \mathbb Z \to R^+$ of additive groups such that $\mu(1)=a$. Then $na$ is simply $\mu(n)$.