CIRCLE WITH A DOT

@johncarlosbaez @jameshanson There is (there has to be, since you just take the data and reassemble it under different notation), but I heavily heavily advise you to not use it because it would be miserable under mathlib's system of conventions. Instead people just duplicate every single theorem proved about groups.
Worth noting that the Rocq proof assistant uses another approach called the Hierarchy Builder where they don't need this duplication.