The concrete products in the category of modules are products in the categorical sense. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
The product cone induced by the concrete product.
The concrete product cone is limiting.
The categorical product of a family of objects in
agrees with the usual module-theoretical product.