prod_instances

Stream: new members

[Scott Morrison]

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]

instance [add_comm_group α] [add_comm_group β] : add_comm_group (α × β) :=
{ .. prod.add_comm_semigroup, .. prod.add_group }

[Kenny Lau]

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

[Ainsley Pahljina]

Thank you Kenny

[Scott Morrison]

(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.)