products of groups?

Stream: maths

[Scott Morrison]

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]

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

[Scott Morrison]

@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]

If not I can do it sometime.

[Patrick Massot]

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?