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