feat(group_theory/submonoid): add `submonoid.powers_one` (#17692)
feat(group_theory/submonoid): add `submonoid.powers_one` (#17692)

* Add `submonoid.powers_one` and `add_submonoid.multiples_zero`.
* Use `to_additive` to generate more proofs.





leanprover-community/mathlib,leanprover-community/mathlib