[Merged by Bors] - feat(ring_theory/polynomial/opposites + data/{polynomial/basic + finsupp/basic}): move op_ring_equiv to a new file + lemmas
#13162
Conversation
adomani
added
the
awaiting-review
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
adomani
changed the title
op_ring_equiv to a new file + lemmasop_ring_equiv to a new file + lemmas
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…mathlib into adomani_op_C
|
I'll add the remaining lemmas, though probably not today! |
semorrison
added
awaiting-author
adomani
added
awaiting-review
|
Eric, I added the lemmas. Let me know if this is not what you had in mind! I also added a couple of doc-module strings to guide through the structure of the (very short) file. |
|
Would you mind merging master? |
|
|
||
| /-! Lemmas to get started, using `(op_ring_equiv R).symm` on the various expressions of | ||
| `finsupp.single`: `monomial`, `C a`, `X`, `C a * X ^ n`. -/ | ||
| @[simp] lemma op_ring_equiv_symm_op_monomial (n : ℕ) (r : Rᵐᵒᵖ) : |
There was a problem hiding this comment.
| @[simp] lemma op_ring_equiv_symm_op_monomial (n : ℕ) (r : Rᵐᵒᵖ) : | |
| @[simp] lemma op_ring_equiv_symm_monomial (n : ℕ) (r : Rᵐᵒᵖ) : |
This lemma and a few below have an op in the name that shouldn't be there
There was a problem hiding this comment.
Thanks! I'll update the names and will also merge master: the change you mentioned made R implicit and I am in the process of fixing it!
There was a problem hiding this comment.
I'm not sure I made R implicit consciously - feel free to keep it explicit
There was a problem hiding this comment.
Actually, you have not: it was some weird issue probably due to old oleans being used instead of the new ones.
There was a problem hiding this comment.
On the topic of explicit vs implicit R: at the moment, R could be made implicit, since there are enough type annotation that it is redundant. However, I feel that using or_ring_equiv is a little bit further below what I would expect to see when actually using an Rᵐᵒᵖ[X]. So, for "regular" usage, it should not matter, since the simp lemmas in this file make or_ring_equiv disappear.
However, if you really want to have control, you may prefer to take the opposite of a subring, rather than the "obvious one" and then having the explicit R could be helpful.
|
I merged master, re-squeezed the first proof for the |
leanprover-community-bot-assistant
added
ready-to-merge
…upp/basic}): move `op_ring_equiv` to a new file + lemmas (#13162) This PR moves the isomorphism `R[X]ᵐᵒᵖ ≃+* Rᵐᵒᵖ[X]` to a new file `ring_theory.polynomial.opposites`. I also proved some basic lemmas about the equivalence. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members)
|
Build failed (retrying...): |
…upp/basic}): move `op_ring_equiv` to a new file + lemmas (#13162) This PR moves the isomorphism `R[X]ᵐᵒᵖ ≃+* Rᵐᵒᵖ[X]` to a new file `ring_theory.polynomial.opposites`. I also proved some basic lemmas about the equivalence. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members)
|
Build failed (retrying...): |
…upp/basic}): move `op_ring_equiv` to a new file + lemmas (#13162) This PR moves the isomorphism `R[X]ᵐᵒᵖ ≃+* Rᵐᵒᵖ[X]` to a new file `ring_theory.polynomial.opposites`. I also proved some basic lemmas about the equivalence. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members)
|
Build failed (retrying...): |
…upp/basic}): move `op_ring_equiv` to a new file + lemmas (#13162) This PR moves the isomorphism `R[X]ᵐᵒᵖ ≃+* Rᵐᵒᵖ[X]` to a new file `ring_theory.polynomial.opposites`. I also proved some basic lemmas about the equivalence. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members)
|
Build failed (retrying...): |
…upp/basic}): move `op_ring_equiv` to a new file + lemmas (#13162) This PR moves the isomorphism `R[X]ᵐᵒᵖ ≃+* Rᵐᵒᵖ[X]` to a new file `ring_theory.polynomial.opposites`. I also proved some basic lemmas about the equivalence. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members)
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
op_ring_equiv to a new file + lemmasop_ring_equiv to a new file + lemmas
This PR moves the isomorphism
R[X]ᵐᵒᵖ ≃+* Rᵐᵒᵖ[X]to a new filering_theory.polynomial.opposites.I also proved some basic lemmas about the equivalence.
Zulip discussion