Commit 2021-04-23 07:17 85df3a36View on Github →
refactor(group_theory/submonoid/basic): merge together similar lemmas and definitions (#7280)
simps to generate lots of uninteresting coe lemmas, and removes the less-bundled versions of definitions.
The main changes are:
add_submonoid.to_submonoid_equivis now just called
add_submonoid.to_submonoid. This means we can remove the
add_submonoid.to_submonoid_monolemma, as that's available as
add_submonoid.to_submonoid.monotone. Ditto for the multiplicative version.
simpsnow knows how to handled
(add_)submonoidobjects. Unfortunately it uses
coeas 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
coeas a suffix.
submonoid.of_add_submonoidhas been renamed to
add_submonoid.to_submonoid'to enable dot notation.
add_submonoid.of_submonoidhas been renamed to
submonoid.to_add_submonoid'to enable dot notation.
- The above points, but applied to
- Two new variants of the closure lemmas about
submonoid.to_add_submonoid'_closure), taken from #7279
deleted def add_submonoid.of_submonoid
deleted theorem add_submonoid.of_submonoid_coe
deleted theorem add_submonoid.of_submonoid_mono
deleted def add_submonoid.submonoid_equiv
deleted theorem add_submonoid.submonoid_equiv_coe
deleted theorem add_submonoid.submonoid_equiv_symm_coe
added def add_submonoid.to_submonoid'
added theorem add_submonoid.to_submonoid'_closure
modified def add_submonoid.to_submonoid
modified theorem add_submonoid.to_submonoid_closure
deleted theorem add_submonoid.to_submonoid_coe
deleted theorem add_submonoid.to_submonoid_mono
deleted def submonoid.add_submonoid_equiv
deleted theorem submonoid.add_submonoid_equiv_coe
deleted theorem submonoid.add_submonoid_equiv_symm_coe
deleted def submonoid.of_add_submonoid
deleted theorem submonoid.of_add_submonoid_coe
deleted theorem submonoid.of_add_submonoid_mono
added def submonoid.to_add_submonoid'
added theorem submonoid.to_add_submonoid'_closure
modified def submonoid.to_add_submonoid
modified theorem submonoid.to_add_submonoid_closure
deleted theorem submonoid.to_add_submonoid_coe
deleted theorem submonoid.to_add_submonoid_mono