direct product of groups

Stream: new members

[LiXiang]

Hi. How can I implement the direct product of groups on Lean (possibly more than two groups)? I have checked algebra.group.prod in mathlib, but it only works for the product of two groups. In my mind, it should be something like \prod (i:I), f i but I don't know the exact syntax.

[Johan Commelin]

@LiXiang Try \pi i, f i.

[Eric Wieser]

Note that under Johan's suggestion single i a * single j b * single i a⁻¹ = single j b. If you don't want this, then you may be after docs#free_product instead.

[LiXiang]

Thank you!