mathlib

fa71e713 - feat(measure_theory/group/add_circle): fundamental domain for rational angle rotations in the circle (#17462)

feat(measure_theory/group/add_circle): fundamental domain for rational angle rotations in the circle (#17462) The main results are `add_circle.is_add_fundamental_domain_of_ae_ball` and its corollary `add_circle.volume_of_add_preimage_eq`.