mathlib

babca8e3 - refactor(algebra/group_with_zero): rename lemmas to use ₀ instead of ' (#9424)

refactor(algebra/group_with_zero): rename lemmas to use ₀ instead of ' (#9424) We currently have lots of lemmas for `group_with_zero` that already have a corresponding lemma for `group`. We've dealt with name collisions so far just by adding a prime. This PR renames these lemmas to use a `₀` suffix instead of a `'`. In part this is out of desire to reduce our overuse of primes in mathlib names (putting the burden on users to know names, rather than relying on naming conventions). But it may also help with a problem Daniel Selsam ran into at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/mathport.20depending.20on.20mathlib. (Briefly, mathport is also adding primes to names when it encounters name collisions, and these particular primes were causing problems. There are are other potential fixes in the works, but everything helps.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>