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

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)$$

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)$.

$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)$.

• But before defining a cyclic group, don't you have to define $a^n$ where the same considerations occur? To prove that $\mu$ is compatible with the addition in $R$, don't you have to define $na$ (or $a^n$) first? – Guest Dec 17 '15 at 2:13
• You only have to do this for $\mathbb Z$, where the properties are a consequence of Peano's axioms. Then $na$ is defined to be $\mu(n)$. – lhf Dec 17 '15 at 8:49
• I mean, how would you show that $\mu$ exists? Here, for example, they use $h^n$ to do so. – Guest Dec 17 '15 at 16:52
• I think you define $\mu$ by induction: $\mu(1)=a$, $\mu(n+1)=a\mu(n)$ and extend to negatives. The point is that this definition is forced onto you if you want a homomorphism. Hence uniqueness. – lhf Dec 17 '15 at 17:21
• Well, then it seems to me like you just use another notation. Instead of writing $na$ as in my question, you write $\mu(n)$ and your recursive definition of $\mu$ corresponds to the one in my question, part (i). It seems to me like you would still have to prove that $\mu(nm)=\mu(n)\mu(m)$ using induction (as in my question, part (ii)). – Guest Dec 17 '15 at 18:05
{"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 1, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0}