feat(group_theory/submonoid/operations): add lemmas (#7219)
feat(group_theory/submonoid/operations): add lemmas (#7219)

Some lemmas about the interaction between additive and multiplicative submonoids.

I provided the two version (from additive to multiplicative and the other way), I am not sure if `@[to_additive]` can automatize this.





leanprover-community/mathlib,leanprover-community/mathlib