Zulip Chat Archive

Stream: new members

Topic: prod_instances


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Oct 03 2019 at 04:29):

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

view this post on Zulip Kenny Lau (Oct 03 2019 at 04:29):

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

view this post on Zulip Ainsley Pahljina (Oct 03 2019 at 05:29):

Thank you Kenny

view this post on Zulip 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