Product of subgroups

Stream: Is there code for X?

[Zhangir Azerbayev]

For subgroups $H, K\leq G$, we can define the product of subgroups $HK = \{hk : h \in H, k\in K\}$. If $HK = KH$, then $HK$ is a subgroup. Is there a convenient way to construct the subgroup instance for $HK$ in mathlib? I am particularly interested in the special case where either $H$ or $K$ is normal (which implies the $HK=KH$ condition).

The pointwise locale allows us to easily construct H*K as a set, but I am interested in the subgroup instance. The file group_theory.coset doesn't seem to contain anything directly useful either.

[Junyan Xu]

docs#subgroup.mul_normal

[Junyan Xu]

seems the answer is to just use H ⊔ K

[Junyan Xu]

Or if you want the underlying set to be definitionally ↑H * ↑K, you may use docs#subgroup.copy

[Zhangir Azerbayev]

Nice! UsingH ⊔ K is sufficient for my purposes, but it is good to know about docs#subgroup.copy.