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).

source

theorem dvd_sub_pow_of_dvd_sub {R : Type u_1} [comm_ring R] {p : ℕ} {a b : R} (h : ↑p ∣ a - b) (k : ℕ) :

↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k