9.4. Congruence for Hensel lifting🔗

Hensel lifting works modulo a prime power, so HexPolyZ carries a coefficientwise congruence predicate and the notion of two polynomials being coprime modulo p.

def

Hex.ZPoly.congr (f g : Hex.ZPoly) (m : ℕ) : Prop
Hex.ZPoly.congr (f g : Hex.ZPoly)
  (m : ℕ) : Prop

Coefficientwise congruence modulo m.

def

Hex.ZPoly.coprimeModP (f g : Hex.ZPoly) (p : ℕ) : Prop
Hex.ZPoly.coprimeModP (f g : Hex.ZPoly)
  (p : ℕ) : Prop

Two integer polynomials are coprime mod p when they admit a Bezout combination congruent to 1 modulo p.

Hex.ZPoly.modP reduces an integer polynomial coefficientwise to an executable polynomial over Hex.ZMod64.

def

Hex.ZPoly.modP (p : ℕ) [Hex.ZMod64.Bounds p] (f : Hex.ZPoly) :
  Hex.FpPoly p
Hex.ZPoly.modP (p : ℕ)
  [Hex.ZMod64.Bounds p] (f : Hex.ZPoly) :
  Hex.FpPoly p

Reduce the coefficients of an integer polynomial modulo p.

The congruence is an equivalence relation and is compatible with the ring operations, so Hensel-step reasoning can rewrite under it.

theorem

Hex.ZPoly.congr_refl (f : Hex.ZPoly) (m : ℕ) : f.congr f m
Hex.ZPoly.congr_refl (f : Hex.ZPoly)
  (m : ℕ) : f.congr f m

Coefficientwise congruence modulo m is reflexive.

theorem

Hex.ZPoly.congr_symm (f g : Hex.ZPoly) (m : ℕ) (hfg : f.congr g m) :
  g.congr f m
Hex.ZPoly.congr_symm (f g : Hex.ZPoly)
  (m : ℕ) (hfg : f.congr g m) :
  g.congr f m

Coefficientwise congruence modulo m is symmetric.

theorem

Hex.ZPoly.congr_trans (f g h : Hex.ZPoly) (m : ℕ) (hfg : f.congr g m)
  (hgh : g.congr h m) : f.congr h m
Hex.ZPoly.congr_trans (f g h : Hex.ZPoly)
  (m : ℕ) (hfg : f.congr g m)
  (hgh : g.congr h m) : f.congr h m

Coefficientwise congruence modulo m is transitive.

theorem

Hex.ZPoly.congr_add (f g f' g' : Hex.ZPoly) (m : ℕ) (hf : f.congr f' m)
  (hg : g.congr g' m) : (f + g).congr (f' + g') m
Hex.ZPoly.congr_add
  (f g f' g' : Hex.ZPoly) (m : ℕ)
  (hf : f.congr f' m)
  (hg : g.congr g' m) :
  (f + g).congr (f' + g') m

Addition preserves coefficientwise congruence modulo m in both inputs.

theorem

Hex.ZPoly.congr_mul (f g f' g' : Hex.ZPoly) (m : ℕ) (hf : f.congr f' m)
  (hg : g.congr g' m) : (f * g).congr (f' * g') m
Hex.ZPoly.congr_mul
  (f g f' g' : Hex.ZPoly) (m : ℕ)
  (hf : f.congr f' m)
  (hg : g.congr g' m) :
  (f * g).congr (f' * g') m

Multiplication preserves coefficientwise congruence modulo m in both inputs.