Zulip Chat Archive

Stream: new members

Topic: direct product of groups


LiXiang (Jul 26 2021 at 13:57):

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 (Jul 26 2021 at 14:10):

@LiXiang Try \pi i, f i.

Eric Wieser (Jul 26 2021 at 14:24):

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 (Jul 26 2021 at 14:27):

Thank you!


Last updated: Dec 20 2023 at 11:08 UTC