mathlib

00024db7 - refactor(group_theory/monoid_localization): use old_structure_cmd (#2683)

refactor(group_theory/monoid_localization): use old_structure_cmd (#2683) Second bit of #2675. The change to ```old_structure_cmd``` is so ring localizations can use this file more easily. I've not made sure the map ```f``` is implicit when it can be because ```f.foo``` notation means it doesn't make much difference, but I'll change this if needed.* I have changed some of the bad names at the end; they are still not great. Does anyone have any alternative suggestions? Things to come in future PRs: the group completion of a comm monoid and some examples, ```away``` (localization at a submonoid generated by one element), more stuff on the localization as a quotient type & the fact it satisfies the char pred. I think I've learnt some stuff about the ```@[simp]``` linter today. Hopefully I'll be making fewer commits trying and failing to appease it. *edit: I mean I haven't checked how many places I can make ```f``` implicit & remove the appropriate ```f.```'s.