mathlib

b2c707cd - feat(group_theory): use generic `subobject_class` lemmas (#11758)

feat(group_theory): use generic `subobject_class` lemmas (#11758) This subobject class refactor PR follows up from #11750 by moving the `{zero,one,add,mul,...}_mem_class` lemmas to the root namespace and marking the previous `sub{monoid,group,module,algebra,...}.{zero,one,add,mul,...}_mem` lemmas as `protected`. This is the second part of #11545 to be split off. I made the subobject parameter to the `_mem` lemmas implicit if it appears in the hypotheses, e.g. ```lean lemma mul_mem {S M : Type*} [monoid M] [set_like S M] [submonoid_class S M] {s : S} {x y : M} (hx : x ∈ s) (hy : y ∈ s) : x * y ∈ s ``` instead of having `(s : S)` explicit. The generic `_mem` lemmas are not namespaced, so there is no dot notation that requires `s` to be explicit. Also there were already a couple of instances for the same operator where `s` was implicit and others where `s` was explicit, so some change was needed.