Commit 2020-05-16 21:18 00024db7

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.