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
b in a commutative ring
R and for
all natural numbers
p ^ (k + 1) divides
a ^ (p ^ k) - b ^ (p ^ k).