flintlib
Definition of irreducibility
At the moment, the *_poly_is_irreducible functions over finite fields say that constant polynomials are irreducible
julia> Fx, x = GF(2)["x"];
julia> is_irreducible(x^0)
true
julia> is_irreducible(0*x)
true
Before I try to fix this, I wanted to ask what the convention is that flint follows. Surely units should not be irreducible, but what about the zero polynomial?
I would say that units are not irreducible.
For these kinds of things lately, I am a great fan of looking at what mathlib says, https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Prime/Defs.html#Irreducible, as they need to choose a consistent definition.
I wasn't even aware that there is a debate to be had here, all text books I looked at agree on this, units and zero are never irreducible.
If one wants a consistent theory of factorization in rings, allowing non-domains, it is common to have a definition that implies that 0 is irreducible in domains.
