mathlib3

4b4e76ca - 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.