mathlib3

d5ca915d - refactor(measure_theory/group/fundamental_domain): Use `pairwise` (#17928)

refactor(measure_theory/group/fundamental_domain): Use `pairwise` (#17928) Replace `∀ g ≠ (1 : G), ae_disjoint μ (g • s) s` ("translates are disjoint to the original set") by the stronger and more symmetric `pairwise (ae_disjoint μ on λ g : G, g • s)` ("translates are disjoint"). In full generality, the latter condition is the one we mean, and indeed this change reduces typeclass assumptions for a few lemmas.