New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(ring_theory/polynomial/basic): Isomorphism between polynomials over a quotient and quotient over polynomials #3847
Conversation
left_inv := by { | ||
intro f, | ||
apply polynomial.induction_on' f, | ||
{ simp_intros p q hp hq, | ||
rw [hp, hq] }, | ||
{ rintros n ⟨x⟩, | ||
simp [monomial_eq_smul_X, C_mul'] } | ||
}, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The style guide recommends using begin ... end
for any multiline proof, and also to not put braces on their own line.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Otherwise, LGTM.
Could you fix the formatting suggestion, and then merge? bors d+ |
✌️ dtumad can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…ver a quotient and quotient over polynomials (#3847) The main statement is `polynomial_quotient_equiv_quotient_polynomial`, which gives that If `I` is an ideal of `R`, then the ring polynomials over the quotient ring `I.quotient` is isomorphic to the quotient of `polynomial R` by the ideal `map C I`. Also, `mem_map_C_iff` shows that `map C I` contains exactly the polynomials whose coefficients all lie in `I`
Pull request successfully merged into master. Build succeeded: |
The main statement is
polynomial_quotient_equiv_quotient_polynomial
, which gives that IfI
is an ideal ofR
, then the ring polynomials over the quotient ringI.quotient
is isomorphic to the quotient ofpolynomial R
by the idealmap C I
.Also,
mem_map_C_iff
shows thatmap C I
contains exactly the polynomials whose coefficients all lie inI
I couldn't find this equivalence anywhere in mathlib already. I created
quotient_map_C_eq_zero
andeval₂_C_mk_eq_zero
just so they could be passed toquotient.lift
as proofs that functions being defined are well defined. If they don't seem generally useful, I can inline them into the definition of the isomorphism, but the definition got very messy when I originally did that.