Commit 2024-01-27 10:41 7f19636c

chore: factor out a lemma from the proof of Steinhaus theorem (#9907) Given a measure in a locally compact group, and a compact set k, then for g close enough to the identity, the set g • k \ k has arbitrarily small measure. A slightly weaker version of this fact is used implicitly in our current proof of Steinhaus theorem that E - E is a neighborhood of the identity if E has positive measure. Since I will need this lemma later on, I extract it from the proof of Steinhaus theorem in this PR.