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

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