mathlib3

feat(geometry/euclidean/congruence): define congruences

#18214

Open