Commit 2021-02-11 16:20 194ec667

feat(group_theory/subgroup): prove relation between pointwise product of submonoids/subgroups and their join (#6165) If H and K are subgroups/submonoids then H ⊔ K = closure (H * K), where H * K is the pointwise set product. When H or K is a normal subgroup, it is proved that (↑(H ⊔ K) : set G) = H * K.

<!-- put comments you want to keep out of the PR commit here. If this PR depends on other PRs, please list them below this comment, using the following format: - [ ] depends on: #abc [optional extra text] - [ ] depends on: #xyz [optional extra text] -->