The Irreduc function is a placeholder for testing the irreducibility of the multivariate polynomial a. It is used in conjunction with mod and modp1.

Formally, an element a of a commutative ring R is said to be "irreducible" if it is not zero, not a unit, and  implies either b or c is a unit.

In this context where R is the ring of polynomials over the integers mod p, which is a finite field, the units are the non-zero constant polynomials. Hence all constant polynomials are not irreducible by this definition.

The call Irreduc(a) mod p returns true iff a is "irreducible" modulo p. The polynomial a must have rational coefficients or coefficients from a finite field specified by RootOf expressions.

The call Irreduc(a, K) mod p returns true iff a is "irreducible" modulo p over the finite field defined by K, an algebraic extension of the integers mod p where K is a RootOf.

The call modp1(Irreduc(a), p) returns true iff a is "irreducible" modulo p. The polynomial a must be in the modp1 representation.