It is also a consequence of P7 (the existence of multiplicative inverses) that if $a \cdot b = 0$ then either $a=0$ or $b=0$.
This is from Calculus, M. Spivak, 2008, chapter 1, "Basic Properties of Numbers". A short proof is given.
Would this statement be considered a lemma? In working thru the chapter 1 exercises, it seems to do an awful lot of work.
In showing when $(x+y)^2 = x^2+y^2$, for example, you end up looking at when $-2xy=0$, so when $xy=0$. By the statement under consideration, your solution is when $x=0$ or $y=0$.
If this statement would be considered a lemma, does it have a name?
Since it is essentially stating "the product zero always has zero among its factors", I have taken to calling it "the Zero Factor Lemma" – but I would like to know if it is already known as something else.
Formally, this statement is known as the Null Factor Law. There are many other variations of this, but all the names refer to the same thing. I am aware that those who were educated in America probably called it the Zero Product as well.
The Null Factor Law is especially useful when dealing with solving quadratics and other polynomials. e.g.
\begin{align} -2 &=x^2-6x+3 \\ 0& = x^2-6x+5\\ & = (x-5)(x-1) \\ \therefore ~&x=5 ~\text{or} ~ x=1 \end{align}