Primitive integer multivariate equations, denominator clearing, and reflection of divisibility from rational coefficients for primitive equations.

def CCDN.PrimitiveIntegerPolynomial {σ : Type u_1} (f : MvPolynomial σ ℤ) : Prop

The integer coefficients have no common nonunit divisor.

Equations

• CCDN.PrimitiveIntegerPolynomial f = ∀ (c : ℤ), (∀ (m : σ →₀ ℕ), c ∣ f.coeff m) → IsUnit c

theorem CCDN.PrimitiveIntegerPolynomial.irreducible_of_rational_map {σ : Type u_1} {f : MvPolynomial σ ℤ} (hf : PrimitiveIntegerPolynomial f) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom ℚ)) f)) : Irreducible f

A primitive integer polynomial whose image over ℚ is irreducible is irreducible over ℤ.

theorem CCDN.mvPolynomial_integer_multiple {σ : Type u_1} (f : MvPolynomial σ ℚ) : ∃ (b : ℤ) (g : MvPolynomial σ ℤ), b ≠ 0 ∧ (MvPolynomial.map (Int.castRingHom ℚ)) g = MvPolynomial.C ↑b * f

Clearing denominators: every rational multivariate polynomial has a nonzero integer multiple b • f with integer coefficients.

theorem CCDN.PrimitiveIntegerPolynomial.rational_map_dvd_iff {σ : Type u_1} {f g : MvPolynomial σ ℤ} (hf : PrimitiveIntegerPolynomial f) : (MvPolynomial.map (Int.castRingHom ℚ)) f ∣ (MvPolynomial.map (Int.castRingHom ℚ)) g ↔ f ∣ g

For any primitive equation, integer divisibility is exactly rational coefficient divisibility.

theorem CCDN.exists_primitive_integer_factor {σ : Type u_1} (f : MvPolynomial σ ℤ) (hf : f ≠ 0) : ∃ (c : ℤ) (g : MvPolynomial σ ℤ), c ≠ 0 ∧ PrimitiveIntegerPolynomial g ∧ f = MvPolynomial.C c * g

Extract a primitive integer equation by the gcd of its nonzero coefficients. The scalar is nonzero.