refactor(algebra/group): make multiplicative and additive irreducible
#2292
Conversation
urkud
commented
Mar 30, 2020
•
urkud
commented
Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
src/algebra/group/type_tags.lean
Outdated
| @@ -13,14 +13,54 @@ variables {α : Type u} {β : Type v} | |||
| def additive (α : Type*) := α | |||
| def multiplicative (α : Type*) := α | |||
There was a problem hiding this comment.
Does @[to_additive additive] work here?
There was a problem hiding this comment.
It seems less duplication to only define it once and have to_additive copy it, but maybe I'm overestimating the savings here.
There was a problem hiding this comment.
I mean, do we want to_additive to turn multiplicative in a lemma into additive? I don't think so. More precisely, I don't think that to_additive will work with a lemma involving both α and multiplicative β.
src/algebra/group/type_tags.lean
Outdated
| def to_add (x : α) : additive α := x | ||
|
|
||
| /-- Reinterpret `x : additive α` as an element of `α`. -/ | ||
| def of_add (x : additive α) : α := x |
There was a problem hiding this comment.
This should probably be in the additive namespace so that field notation works.
There was a problem hiding this comment.
What rename do you propose?
There was a problem hiding this comment.
additive.to_mul is the best that I can think of now.
There was a problem hiding this comment.
Just to be sure that I understand correctly: do you propose __root__.to_mul, additive.to_mul, __root__.to_add and multiplicative.to_add? If we want to avoid polluting the __root__ namespace, we can use additive.of_mul, additive.to_mul, multiplicative.of_add and multiplicative.to_add.
There was a problem hiding this comment.
I don't think @gebner is worried about pollution, but rather wants to enable writing x.to_mul for x : additive foo.
There was a problem hiding this comment.
@jcommelin That's right. This is the definition I'm proposing:
def additive.to_mul (x : additive α) : α := xThere was a problem hiding this comment.
Then we should move to_mul to multiplicative.of_add because otherwise we'll have __root__.to_mul and additive.to_mul, and it will be hard to tell whether we go α → multiplicative α or additive α → α.
I think that I'll make a version of this PR that doesn't add irreducible but adds to_mul and of_mul + simp lemmas.
There was a problem hiding this comment.
The naming of this function was just a suggestion. I still think that this PR makes the right choice in making multiplicative and additive irreducible.
There was a problem hiding this comment.
It leads to quite a few build failures. I want to merge to_mul/of_mul/to_add/of_add before fixing these failures.
github-actions
bot
added
the
merge-conflict
|
Since #2363 is in, can this be revived? |
There are some parts of mathlib (e.g., |
github-actions
bot
removed
the
merge-conflict
github-actions
bot
added
the
merge-conflict
