Commit 2025-10-06 12:00 3681a104

chore: new file for constructions of uniform groups (#30026) The split between Defs and Basic was a bit messy (e.g the Prod instance was in Defs but the Pi instance was in Basic), and I'm going to make these files longer when introducing left and right uniform groups, so I figured the best solution was to move everything in an intermediate Constructions file.