Definition of irreducibility

[thofma]

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?

[edgarcosta]

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.

[fingolfin]

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.

[thofma]

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.

[fredrik-johansson]

Agree with following mathlib.

[albinahlback]

Related to #2094