Documentation

Mathlib.NumberTheory.Basic

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 : R} {b : R} (h : p a - b) (k : ) :
p ^ (k + 1) a ^ p ^ k - b ^ p ^ k