Positive-degree irreducible integer equations remain irreducible over Q. Primitive denominator-cleared divisors give an elementary Gauss argument.

theorem CCDN.rational_map_irreducible_of_integer {n : ℕ} (f : MvPolynomial (Fin n) ℤ) (hir : Irreducible f) (hd : 0 < f.totalDegree) : Irreducible ((MvPolynomial.map (Int.castRingHom ℚ)) f)

An irreducible integer polynomial of positive total degree remains irreducible over ℚ.