## Stream: new members

### Topic: prod_instances

#### Scott Morrison (Oct 03 2019 at 04:25):

Where are the product instances? E.g. if I have an add_comm_group on X and on Y, and want it on X \times Y?

#### Kenny Lau (Oct 03 2019 at 04:29):

instance [add_comm_group α] [add_comm_group β] : add_comm_group (α × β) :=


#### Kenny Lau (Oct 03 2019 at 04:29):

https://github.com/leanprover-community/mathlib/blob/master/src/algebra/pi_instances.lean#L231

Thank you Kenny

#### Scott Morrison (Oct 03 2019 at 05:54):

(Somehow I had been sure that there was a file called prod_instances, and when we couldn't find it I didn't think to look carefully through pi_instances.)

Last updated: May 10 2021 at 19:16 UTC