Basic results in number theory #
This file should contain basic results in number theory. So far, it only contains the essential lemma in the construction of the ring of Witt vectors.
Main statement #
dvd_sub_pow_of_dvd_sub proves that for elements a and b in a commutative ring R and for
all natural numbers p and k if p divides a-b in R, then p ^ (k + 1) divides
a ^ (p ^ k) - b ^ (p ^ k).
theorem
dvd_sub_pow_of_dvd_sub
{R : Type u_1}
[CommRing R]
{p : ℕ}
{a b : R}
(h : ↑p ∣ a - b)
(k : ℕ)
:
↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k