ヘンゼルの補題
が成り立つ。これから、ある2進整数 b で
b 2 = 17 and | b − a | 2 < | f ′ ( a ) | 2 = 1 2 {\displaystyle b^{2}=17\quad {\text{and}}\quad |b-a|_{2}<|f'(a)|_{2}={\frac {1}{2}}}
を満たすものが一意に存在する。二番目の式は b ≡ 1 mod 4 を意味する。2進整数の中には17の平方根が2つ存在し、それらは符号が異なり、法2では合同であるが法4では合同ではない。これは、一般化された形のヘンゼルの補題から得られるのが法2ではなく法4で1と合同な17の2進平方根で、法4で一意であることと整合的である。最初の近似根として a = 3 を取った場合でも一般化されたヘンゼルの補題を適用することができ、法4で3と合同になる唯一の17の2進平方根をやはり見つけることができる。これがもう1つの17の2進平方根である。
x 2 − 17 {\displaystyle x^{2}-17} の根を法 2 から法 2 へ持ち上げるやり方の場合、法2での根1からの持ち上げの過程は次のようになる。
1 mod 2 は 1, 3 mod 4 に持ち上がる。
1 mod 4 は 1, 5 mod 8 に、3 mod 4 は 3, 7 mod 8 に持ち上がる。
1 mod 8 は 1, 9 mod 16 に、7 mod 8 は 7, 15 mod 16 に持ち上がる。一方、3 mod 8 と 5 mod 8 は mod 16 での根に持ち上がらない。
9 mod 16 は 9, 25 mod 32 に、7 mod 16 は 7, 23 mod 16 に持ち上がる。
f ( s ) ≡ 0 mod p k + m ⟺ ( z + t f ′ ( r ) ) p k ≡ 0 mod p k + m ⟺ z + t f ′ ( r ) ≡ 0 mod p m ⟺ t f ′ ( r ) ≡ − z mod p m ⟺ t ≡ − z [ f ′ ( r ) ] − 1 mod p m p ∤ f ′ ( r ) {\displaystyle {\begin{aligned}f(s)\equiv 0{\bmod {p}}^{k+m}&\Longleftrightarrow (z+tf'(r))p^{k}\equiv 0{\bmod {p}}^{k+m}\\&\Longleftrightarrow z+tf'(r)\equiv 0{\bmod {p}}^{m}\\&\Longleftrightarrow tf'(r)\equiv -z{\bmod {p}}^{m}\\&\Longleftrightarrow t\equiv -z[f'(r)]^{-1}{\bmod {p}}^{m}&&p\nmid f'(r)\end{aligned}}}
である。 f ′ ( r ) {\displaystyle f'(r)} は p で割り切れないという仮定から、 f ′ ( r ) {\displaystyle f'(r)} は法 p m {\displaystyle p^{m}} で逆元を持ち、しかもそれは一意でなければならない。したがって、最後の式の t についての解は法 p m {\displaystyle p^{m}} で一意に存在し、s は法 p k + m {\displaystyle p^{k+m}} で一意に存在する。
a ∈ F p {\displaystyle a\in \mathbb {F} _{p}} に対してフロベニウス自己準同型 ( − ) ↦ ( − ) p {\displaystyle (-)\mapsto (-)^{p}} による多項式 x p − a {\displaystyle x^{p}-a} を考える。この微分は
d d x x p − a = p ⋅ x p − 1 ≡ 0 ⋅ x p − 1 mod p ≡ 0 mod p {\displaystyle {\begin{aligned}{\frac {d}{dx}}x^{p}-a&=p\cdot x^{p-1}\\&\equiv 0\cdot x^{p-1}{\bmod {p}}\\&\equiv 0{\bmod {p}}\end{aligned}}}
となり常にゼロである。したがって a {\displaystyle a} の p 乗根は Z p {\displaystyle \mathbb {Z} _{p}} に存在しない。 a = 1 {\displaystyle a=1} の場合、これは Z p {\displaystyle \mathbb {Z} _{p}} には1の冪根 μ p {\displaystyle \mu _{p}} が含まれないことを意味する。