mathlib

194ec667 - feat(group_theory/subgroup): prove relation between pointwise product of submonoids/subgroups and their join (#6165)

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