mathlib3

678566f2 - feat(topology/algebra/group): Addition of interiors (#10659)

feat(topology/algebra/group): Addition of interiors (#10659) This proves `interior s * t ⊆ interior (s * t)`, a few prerequisites, and generalizes to `is_open.mul_left`/`is_open.mul_right`.