Basic results in number theory #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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)
.