@antoinechambertloir@mathstodon.xyz
Post #1366380
2025-04-06 21:15 UTC
(#math thread)
Recently, in the Zulip server for Lean users, somebody went with something that looked like homework, but managed to sting me a little bit.
It was about irreducibility of polynomials with integer coefficients. Specifically, the guy wanted a proof that the polynomial T^4-10 T^2+1 is irreducible, claiming that the Eisenstein criterion was not good at it.
What was to proven (this is what *irreducible* means) is that it is impossible to write that polynomial as the product of two polynomials with integer coefficients, except by writing
T^4-10 T^2+1 as (1)·(T^4-10 T^2+1) or as (-1)·(-T^4+10 T^2-1).
Replies (1)
-
@antoinechambertloir@mathstodon.xyz 2025-04-06 21:20
This is both a complicated and a trivial question. Trivial because there are general bounds (initially due to Mignotte) for the integers that appear in any such factorization, and it could just be sufficient to try any possibility in the given range and conclude. Brute force, not very intelligent, but with a certain outcome. Complicated because those computations would often be long, and there are many criteria in number theory to assert irreducibility. One of the easiest to apply is the aforementioned Eisenstein criterion.