polynomial.eq_of_monic_of_associated

Stream: Is there code for X?

[Kenny Lau]

import data.polynomial

universe u

namespace polynomial

theorem eq_of_monic_of_associated {R : Type u} [integral_domain R] {p q : polynomial R}
  (hp : p.monic) (hq : q.monic) (hpq : associated p q) : p = q :=
sorry

end polynomial

[Kenny Lau]

import data.polynomial

universe u

namespace polynomial

theorem eq_of_monic_of_associated {R : Type u} [integral_domain R] {p q : polynomial R}
  (hp : p.monic) (hq : q.monic) (hpq : associated p q) : p = q :=
begin
  obtain ⟨u, hu⟩ := hpq,
  unfold monic at hp hq,
  rw eq_C_of_degree_le_zero (le_of_eq $ degree_coe_units _) at hu,
  rw [← hu, leading_coeff_mul, hp, one_mul, leading_coeff_C] at hq,
  rwa [hq, C_1, mul_one] at hu
end

end polynomial

[Sebastien Gouezel]

In maths papers, usually before a theorem there is a sentence explaining what the theorem is about, and after the theorem there is a discussion of the shortcomings of the theorem, the relevant examples, and so on, to help the reader figure out why the theorem is interesting. Arguably, all this is already implicit in the statement of the theorem, but still it helps a lot the readers (and it is a little bit more of work for the author)!

Zulip posts should probably be constructed in the same way: instead of a bare code block, sentences explaining the issue and the context would help a lot :)

[Kenny Lau]

If two polynomials (in an integral domain) are monic and divide each other then they are the same polynomial