feat(number_theory/basic): dvd_sub_pow_of_dvd_sub (#2640)

Co-authored with: Kenny Lau <kc_kennylau@yahoo.com.hk>

src/algebra/geom_sum.lean

@@ -78,6 +78,15 @@ begin
     rw[mul_assoc, ← mul_add y, ih] }
 end
 
+theorem geom_series₂_self {α : Type*} [comm_ring α] (x : α) (n : ℕ) :
+  geom_series₂ x x n = n * x ^ (n-1) :=
+calc  (finset.range n).sum (λ i, x ^ i * x ^ (n - 1 - i))
+    = (finset.range n).sum (λ i, x ^ (i + (n - 1 - i))) : by simp_rw [← pow_add]
+... = (finset.range n).sum (λ i, x ^ (n - 1)) : finset.sum_congr rfl
+  (λ i hi, congr_arg _ $ nat.add_sub_cancel' $ nat.le_pred_of_lt $ finset.mem_range.1 hi)
+... = add_monoid.smul (finset.range n).card (x ^ (n - 1)) : finset.sum_const _
+... = n * x ^ (n - 1) : by rw [finset.card_range, add_monoid.smul_eq_mul]
+
 /-- $x^n-y^n = (x-y) \sum x^ky^{n-1-k}$ reformulated without `-` signs. -/
 theorem geom_sum₂_mul_add [comm_semiring α] (x y : α) (n : ℕ) :
   (geom_series₂ (x + y) y n) * x + y ^ n = (x + y) ^ n :=
@@ -152,3 +161,13 @@ begin
     ← mul_assoc, ← mul_assoc, mul_inv_cancel h₃],
   simp [mul_add, add_mul, mul_inv_cancel hx0, mul_assoc, h₄, sub_eq_add_neg, add_comm, add_left_comm],
 end
+
+variables {β : Type*}
+
+theorem ring_hom.map_geom_series [semiring α] [semiring β] (x : α) (n : ℕ) (f : α →+* β) :
+  f (geom_series x n) = geom_series (f x) n :=
+by { rw [geom_series_def, geom_series_def, ← finset.sum_hom _ f], simp_rw [f.map_mul, f.map_pow] }
+
+theorem ring_hom.map_geom_series₂ [semiring α] [semiring β] (x y : α) (n : ℕ) (f : α →+* β) :
+  f (geom_series₂ x y n) = geom_series₂ (f x) (f y) n :=
+by { rw [geom_series₂_def, geom_series₂_def, ← finset.sum_hom _ f], simp_rw [f.map_mul, f.map_pow] }

src/number_theory/basic.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2020 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin, Kenny Lau
+-/
+
+import algebra.geom_sum
+import ring_theory.ideals
+
+section
+
+open ideal ideal.quotient
+
+lemma dvd_sub_pow_of_dvd_sub {R : Type*} [comm_ring R] {p : ℕ}
+  {a b : R} (h : (p : R) ∣ a - b) (k : ℕ) :
+  (p^(k+1) : R) ∣ a^(p^k) - b^(p^k) :=
+begin
+  induction k with k ih,
+  { rwa [pow_one, nat.pow_zero, pow_one, pow_one] },
+  rw [nat.pow_succ, pow_mul, pow_mul, ← geom_sum₂_mul, pow_succ],
+  refine mul_dvd_mul _ ih,
+  let I : ideal R := span {p},
+  let f : R →+* ideal.quotient I := mk_hom I,
+  have hp : (p : ideal.quotient I) = 0,
+  { rw [← f.map_nat_cast, ← mk_eq_mk_hom, eq_zero_iff_mem, mem_span_singleton] },
+  rw [← mem_span_singleton, ← ideal.quotient.eq, mk_eq_mk_hom, mk_eq_mk_hom] at h,
+  rw [← mem_span_singleton, ← eq_zero_iff_mem, mk_eq_mk_hom, ring_hom.map_geom_series₂,
+      ring_hom.map_pow, ring_hom.map_pow, h, geom_series₂_self, hp, zero_mul],
+end
+
+end

src/ring_theory/ideals.lean

@@ -216,6 +216,8 @@ instance (I : ideal α) : comm_ring I.quotient :=
 /-- `ideal.quotient.mk` as a `ring_hom` -/
 def mk_hom (I : ideal α) : α →+* I.quotient := ⟨mk I, rfl, λ _ _, rfl, rfl, λ _ _, rfl⟩
 
+lemma mk_eq_mk_hom (I : ideal α) (x : α) : ideal.quotient.mk I x = ideal.quotient.mk_hom I x := rfl
+
 def map_mk (I J : ideal α) : ideal I.quotient :=
 { carrier := mk I '' J,
   zero := ⟨0, J.zero_mem, rfl⟩,