Hi @FabricioOlivetti, thanks for adding the clarifications.

I'm also interested to add to it a formal proof. That's going to have to begin by restating the general definition of what it means to be a product in a category, and then moving on to show why the gcd satisfies that definition. I don't have much time for this in the short term. But if anyone wants to start giving it a shot now, that would be great...