mathlib3

bfc28c4b - feat(measure_theory/group/fundamental_domain): Interior of a fundamental domain (#17533)

feat(measure_theory/group/fundamental_domain): Interior of a fundamental domain (#17533) Define the interior and frontier of a fundamental domain. Co-authored-by: Alex- J. Best <alex.j.best@gmail.com>