Commit 2022-04-10 01:48 b2c707cd

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.

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.