Commit 2025-11-12 12:36 701ecbf1
View on Github →chore: rename IsTopologicalGroup.toUniformSpace to IsTopologicalGroup.rightUniformSpace (#30009)
I have plans to finally do left and right uniformities properly, but I'd like to do some of the remaining before the fact to ease review.
I also take this opportunity to remove a duplication of private lemmas extend_Z_bilin_aux and extend_Z_bilin_key.