## Stream: Is there code for X?

### Topic: polynomial.eq_of_monic_of_associated

#### Kenny Lau (May 24 2020 at 07:58):

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 (May 24 2020 at 08:10):

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 (May 24 2020 at 08:13):

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 (May 24 2020 at 08:16):

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

Last updated: May 17 2021 at 15:13 UTC