Commit 2021-10-01 03:25 babca8e3

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.)