[Merged by Bors] - chore(*/centralizer): add forgotten to_additives
#19168
Conversation
ericrbg
added
awaiting-review
| @@ -100,10 +100,12 @@ end | |||
| lemma centralizer_subset [has_mul M] (h : S ⊆ T) : centralizer T ⊆ centralizer S := | |||
| λ t ht s hs, ht s (h hs) | |||
|
|
|||
| @[to_additive add_center_subset_add_centralizer] | |||
There was a problem hiding this comment.
What name does to_additive generate here? Why does it generate a wrong name here and generates a correct name for center_le_centralizer?
There was a problem hiding this comment.
It gives the same name. I'm not sure why later on it's not an issue, maybe when a section closes the database for to_additive updates, or the like. I think it's the same in lean4
There was a problem hiding this comment.
and generates a correct name for
center_le_centralizer?
Because the correct additivized name for subgroup.center_le_centralizer is add_subsemigroup.center_le_centralizer, there's no need to replace centralizer with add_centralizer.
Only the set lemmas need these renames.
github-actions
bot
removed
the
awaiting-CI
leanprover-community-bot-assistant
added
ready-to-merge
I forgot these in #18861. These are already in the forward-port PR, leanprover-community/mathlib4#4896.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
to_additivesto_additives
I forgot to put some required `to_additive`s in Lean3, I am currently backporting this change in leanprover-community/mathlib#19168. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
…4896) I forgot to put some required `to_additive`s in Lean3, I am currently backporting this change in leanprover-community/mathlib#19168. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
I forgot these in #18861. These are already in the forward-port PR, leanprover-community/mathlib4#4896.