Zulip Chat Archive

Stream: maths

Topic: products of groups?


view this post on Zulip Scott Morrison (Jun 25 2018 at 02:22):

Do we have instances that provide (pairwise) products of groups in mathlib? I know about pi_instances for indexed products, but can't find anything for the pairwise case.

view this post on Zulip Mario Carneiro (Jun 25 2018 at 02:36):

I think Patrick might have a local version, but it's pretty easy to define in any case.

view this post on Zulip Scott Morrison (Jun 25 2018 at 03:27):

@Patrick Massot, do you have any plans to PR the instances for pairwise products of the basic algebraic hierarchy? (My preference is that there is not a single file with all of these, but they happen in each of the relevant files --- as we add more algebra we'll have to add things like this all along the way.)

view this post on Zulip Scott Morrison (Jun 25 2018 at 03:27):

If not I can do it sometime.

view this post on Zulip Patrick Massot (Jun 25 2018 at 12:21):

All mathlib product instances are hidden in https://github.com/leanprover/mathlib/blob/master/linear_algebra/prod_module.lean, in particular product groups. At some point I tried to move them when preparing a PR but I gave up because everything broke?


Last updated: May 14 2021 at 19:21 UTC