pointwise): add the pointwise monoid structure on `add_submonoid` (#15052)

Commit

3 years ago

feat(group_theory/submonoid/pointwise): add the pointwise monoid structure on `add_submonoid` (#15052) This also adds some missing lemmas about powers of submodules.

Author

eric-wieser

Parents

3644fef6

mathlib 9365548b - feat(group_theory/submonoid/pointwise): add the pointwise monoid structure on `add_submonoid` (#15052)

mathlib
9365548b - feat(group_theory/submonoid/pointwise): add the pointwise monoid structure on `add_submonoid` (#15052)