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.
