[Merged by Bors] - refactor: Int.negOnePow as a map to ℤˣ rather than ℤ#8307
[Merged by Bors] - refactor: Int.negOnePow as a map to ℤˣ rather than ℤ#8307
Conversation
eric-wieser
left a comment
There was a problem hiding this comment.
I can't yet tell what the impact of the negOnePow change is, but these module instance all look like a good idea anyway.
I think just the question about smul_comm instances is left to resolve.
|
Thanks 🎉 bors merge |
Following #7866, `Int.negOnePow` is redefined as a map `ℤ → ℤˣ` rather than `ℤ → ℤ`.
Mathlib/Algebra/Module/Basic.lean
Outdated
| simp [add_smul, sub_eq_add_neg] | ||
| #align sub_smul sub_smul | ||
|
|
||
| instance : SMulCommClass ℤˣ R M where |
There was a problem hiding this comment.
I'm pretty sure we already have these instances more generally; I'll remove them in a follow up
There was a problem hiding this comment.
Actually,I had time to push a fix
|
Canceled. |
Mathlib/Algebra/Module/Basic.lean
Outdated
| instance {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] | ||
| [Module R M] : SMulCommClass ℤˣ R M := inferInstance | ||
|
|
||
| instance {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] |
There was a problem hiding this comment.
This can probably be deleted unless there's a performance issue
eric-wieser
left a comment
There was a problem hiding this comment.
bors d+
I pushed a commit removing the new Units Int lemma entirey; the instances already existed further down in the same file, and the lemma was actually less direct than an existing lemma.
|
✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Thanks! bors merge |
Following #7866, `Int.negOnePow` is redefined as a map `ℤ → ℤˣ` rather than `ℤ → ℤ`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
Following #7866, `Int.negOnePow` is redefined as a map `ℤ → ℤˣ` rather than `ℤ → ℤ`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Following #7866, `Int.negOnePow` is redefined as a map `ℤ → ℤˣ` rather than `ℤ → ℤ`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Following #7866, `Int.negOnePow` is redefined as a map `ℤ → ℤˣ` rather than `ℤ → ℤ`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Following #7866,
Int.negOnePowis redefined as a mapℤ → ℤˣrather thanℤ → ℤ.