theorem HexHenselMathlib.coeff_map_intCastRingHom_eq_zero_iff_dvd (f : Polynomial ℤ) (p n : ℕ) : (Polynomial.map (Int.castRingHom (ZMod p)) f).coeff n = 0 ↔ ↑p ∣ f.coeff n

Reducing an integer coefficient modulo p gives zero exactly when p divides it.

theorem HexHenselMathlib.coeff_map_intCastRingHom_eq_iff_dvd_sub (f g : Polynomial ℤ) (p n : ℕ) : (Polynomial.map (Int.castRingHom (ZMod p)) f).coeff n = (Polynomial.map (Int.castRingHom (ZMod p)) g).coeff n ↔ ↑p ∣ f.coeff n - g.coeff n

Equality after coefficientwise reduction modulo p is equivalent to divisibility of the coefficient difference.

theorem HexHenselMathlib.coeff_ediv_mul_eq_of_dvd {f : Polynomial ℤ} {m n : ℕ} (h : ↑m ∣ f.coeff n) : f.coeff n / ↑m * ↑m = f.coeff n

Exact divisibility lets us recover an integer coefficient from its quotient.

theorem HexHenselMathlib.coeff_mul_ediv_eq_of_dvd {f : Polynomial ℤ} {m n : ℕ} (h : ↑m ∣ f.coeff n) : ↑m * (f.coeff n / ↑m) = f.coeff n

Exact divisibility also gives the left-multiplication form used in coefficientwise quotient rewrites.

theorem HexHenselMathlib.zmod_castHom_comp_intCastRingHom_pow_succ (p k : ℕ) : (ZMod.castHom ⋯ (ZMod p)).comp (Int.castRingHom (ZMod (p ^ (k + 1)))) = Int.castRingHom (ZMod p)

Reducing coefficients from ZMod (p^(k+1)) to ZMod p agrees with direct reduction.

theorem HexHenselMathlib.zmod_castHom_comp_intCastRingHom_pow_step (p k : ℕ) : (ZMod.castHom ⋯ (ZMod (p ^ k))).comp (Int.castRingHom (ZMod (p ^ (k + 1)))) = Int.castRingHom (ZMod (p ^ k))

Reducing coefficients from ZMod (p^(k+1)) to ZMod (p^k) agrees with direct reduction.

theorem HexHenselMathlib.polynomial_map_zmod_pow_succ_to_base (f : Polynomial ℤ) (p k : ℕ) : Polynomial.map (ZMod.castHom ⋯ (ZMod p)) (Polynomial.map (Int.castRingHom (ZMod (p ^ (k + 1)))) f) = Polynomial.map (Int.castRingHom (ZMod p)) f

Polynomial reduction from ZMod (p^(k+1)) to ZMod p is compatible with direct reduction.

theorem HexHenselMathlib.polynomial_map_zmod_pow_succ_to_pow (f : Polynomial ℤ) (p k : ℕ) : Polynomial.map (ZMod.castHom ⋯ (ZMod (p ^ k))) (Polynomial.map (Int.castRingHom (ZMod (p ^ (k + 1)))) f) = Polynomial.map (Int.castRingHom (ZMod (p ^ k))) f

Polynomial reduction from ZMod (p^(k+1)) to ZMod (p^k) is compatible with direct reduction.

theorem HexHenselMathlib.isUnit_one_add_C_mul (p k : ℕ) (u : Polynomial (ZMod (p ^ k))) : IsUnit (1 + Polynomial.C ↑p * u)

In Polynomial (ZMod (p^k)), the correction term p * u is nilpotent, so 1 + p * u is a unit.

theorem HexHenselMathlib.coprime_mod_p_lifts (g h : Polynomial ℤ) (p k : ℕ) [Fact (Nat.Prime p)] (_hk : 0 < k) : IsCoprime (Polynomial.map (Int.castRingHom (ZMod p)) g) (Polynomial.map (Int.castRingHom (ZMod p)) h) → IsCoprime (Polynomial.map (Int.castRingHom (ZMod (p ^ k))) g) (Polynomial.map (Int.castRingHom (ZMod (p ^ k))) h)

Coprimality modulo p lifts to coprimality modulo p^k.

The 0 < k hypothesis is part of the calling convention; the proof does not need it (the k = 0 case is vacuous because ZMod 1 is the zero ring).

theorem HexHenselMathlib.isCoprime_cancel_of_natDegree_lt {R : Type u_1} [CommRing R] [IsDomain R] {g h a b : Polynomial R} (hg : g.Monic) (hcop : IsCoprime g h) (heq : a * h + b * g = 0) (hdeg : a.natDegree < g.natDegree) : a = 0 ∧ b = 0

Coprime monic cancellation with a strict degree bound.

If a * h + b * g = 0 in R[X] for a commutative domain R, where g is monic and IsCoprime g h, then a.natDegree < g.natDegree forces both a = 0 and b = 0.

This is the load-bearing analytic step for the binary-Hensel uniqueness theorem hensel_unique (HexHenselMathlib/Correctness.lean): after reducing the integer-polynomial difference equation modulo p, the problem becomes a coprime cancellation in Polynomial (ZMod p), with the strict degree bound following from the monicity of both g and g' at the same natDegree.