AddgroupClass

Stream: new members

[Yi.Yuan]

I have some issues when I use addgroupclass :
Basic.lean
RingHomInduceFilterHom.lean
I have a map

$$A \to B , \implies \text{there induced a map between filtrations} FA \to FB$$

I want to show each σA mapsto a addsubgroup which is in σB type, should I use a class like this to describe σA and σB?

class SubmonoidClassHom (f : A → B) where
  map : σA → σB
  image_coe_eq_coe_map (x : σA) : f '' (x : Set A) = map x

I don't think mathlib will merge these .