feat(algebra/star/prod): elementwise `star` operator (#13856)
The lemmas and instances this provides are inspired by `algebra/star/pi`, and appear in the same order.
We should have these instances anyway for completness, but the motivation is to make it easy to talk about the continuity of `star` on `units R` via the `units.embed_product_star` lemma.
