# Commit 2021-04-23 07:17 85df3a36

View on Github →refactor(group_theory/submonoid/basic): merge together similar lemmas and definitions (#7280)
This uses `simps`

to generate lots of uninteresting coe lemmas, and removes the less-bundled versions of definitions.
The main changes are:

`add_submonoid.to_submonoid_equiv`

is now just called`add_submonoid.to_submonoid`

. This means we can remove the`add_submonoid.to_submonoid_mono`

lemma, as that's available as`add_submonoid.to_submonoid.monotone`

. Ditto for the multiplicative version.`simps`

now knows how to handled`(add_)submonoid`

objects. Unfortunately it uses`coe`

as a suffix rather than a prefix, so we can't use it everywhere yet. For now we restrict its use to just these additive / multiplicative lemmas which already had`coe`

as a suffix.`submonoid.of_add_submonoid`

has been renamed to`add_submonoid.to_submonoid'`

to enable dot notation.`add_submonoid.of_submonoid`

has been renamed to`submonoid.to_add_submonoid'`

to enable dot notation.- The above points, but applied to
`(add_)subgroup`

- Two new variants of the closure lemmas about
`add_submonoid`

(`add_submonoid.to_submonoid'_closure`

and`submonoid.to_add_submonoid'_closure`

), taken from #7279