## Stream: maths

### Topic: products of groups?

#### 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.

#### 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.

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

#### Scott Morrison (Jun 25 2018 at 03:27):

If not I can do it sometime.

#### 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