Funnily enough, the traditional formal definition of product is due to Peano and it would say 5x3=5+5+5: https://en.m.wikipedia.org/wiki/Peano_axioms#Multiplication
The definition of multiplication is indeed in the Wikipedia article, but if you reread it then you'll see it doesn't claim to be a Paeno axiom. A better article to read (after reading about Paeno axioms!) is here:
https://en.m.wikipedia.org/wiki/Second-order_arithmetic#Basi...