Commit 2022-12-16 11:04 d5ca915d

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.