hex

10.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 : Nat) : Prop
Hex.ZPoly.congr (f g : Hex.ZPoly)
  (m : Nat) : Prop

Coefficientwise congruence modulo m.

🔗def
Hex.ZPoly.coprimeModP (f g : Hex.ZPoly) (p : Nat) : Prop
Hex.ZPoly.coprimeModP (f g : Hex.ZPoly)
  (p : Nat) : Prop

Two integer polynomials are coprime mod p when they admit a Bezout combination congruent to 1 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 : Nat) : f.congr f m
Hex.ZPoly.congr_refl (f : Hex.ZPoly)
  (m : Nat) : f.congr f m

Coefficientwise congruence modulo m is reflexive.

🔗theorem
Hex.ZPoly.congr_symm (f g : Hex.ZPoly) (m : Nat) (hfg : f.congr g m) :
  g.congr f m
Hex.ZPoly.congr_symm (f g : Hex.ZPoly)
  (m : Nat) (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 : Nat) (hfg : f.congr g m)
  (hgh : g.congr h m) : f.congr h m
Hex.ZPoly.congr_trans (f g h : Hex.ZPoly)
  (m : Nat) (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 : Nat)
  (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 : Nat)
  (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 : Nat)
  (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 : Nat)
  (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.