mathlib

d9a6e478 - feat(measure_theory/group): regular, invariant, and conjugate measures (#3650)

feat(measure_theory/group): regular, invariant, and conjugate measures (#3650) Define the notion of a regular measure. I did this in Borel space, which required me to add an import measure_space -> borel_space. Define left invariant and right invariant measures for groups Define the conjugate measure, and show it is left invariant iff the original is right invariant