feat: The Erdős–Ginzburg–Ziv theorem (#14000)

Prove the Erdős–Ginzburg–Ziv theorem as a corollary of Chevalley-Warning. This theorem states that among any (not necessarily distinct) `2 * n - 1` elements of `ZMod n`, we can find `n` elements of sum zero.

Mathlib.lean

@@ -1841,6 +1841,7 @@ import Mathlib.Combinatorics.Additive.Corner.Roth
 import Mathlib.Combinatorics.Additive.Dissociation
 import Mathlib.Combinatorics.Additive.ETransform
 import Mathlib.Combinatorics.Additive.Energy
+import Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
 import Mathlib.Combinatorics.Additive.FreimanHom
 import Mathlib.Combinatorics.Additive.PluenneckeRuzsa
 import Mathlib.Combinatorics.Additive.RuzsaCovering

Mathlib/Algebra/MvPolynomial/Degrees.lean

@@ -435,6 +435,10 @@ theorem totalDegree_finset_sum {ι : Type*} (s : Finset ι) (f : ι → MvPolyno
   · rw [Finset.sum_cons, Finset.sup_cons, sup_eq_max]
     exact (MvPolynomial.totalDegree_add _ _).trans (max_le_max le_rfl hind)
 
+lemma totalDegree_finsetSum_le {ι : Type*} {s : Finset ι} {f : ι → MvPolynomial σ R} {d : ℕ}
+    (hf : ∀ i ∈ s, (f i).totalDegree ≤ d) : (s.sum f).totalDegree ≤ d :=
+  (totalDegree_finset_sum ..).trans $ Finset.sup_le hf
+
 lemma degreeOf_le_totalDegree (f : MvPolynomial σ R) (i : σ) : f.degreeOf i ≤ f.totalDegree :=
   degreeOf_le_iff.mpr fun d hd ↦ (eq_or_ne (d i) 0).elim (·.trans_le zero_le') fun h ↦
     (Finset.single_le_sum (fun _ _ ↦ zero_le') <| Finsupp.mem_support_iff.mpr h).trans

Mathlib/Combinatorics/Additive/ErdosGinzburgZiv.lean

@@ -0,0 +1,203 @@
+/-
+Copyright (c) 2023 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import Mathlib.Algebra.BigOperators.Ring
+import Mathlib.Data.Multiset.Fintype
+import Mathlib.FieldTheory.ChevalleyWarning
+import Mathlib.RingTheory.UniqueFactorizationDomain
+
+/-!
+# The Erdős–Ginzburg–Ziv theorem
+
+This file proves the Erdős–Ginzburg–Ziv theorem as a corollary of Chevalley-Warning. This theorem
+states that among any (not necessarily distinct) `2 * n - 1` elements of `ZMod n`, we can find `n`
+elements of sum zero.
+
+## Main declarations
+
+* `Int.erdos_ginzburg_ziv`: The Erdős–Ginzburg–Ziv theorem stated using sequences in `ℤ`
+* `ZMod.erdos_ginzburg_ziv`: The Erdős–Ginzburg–Ziv theorem stated using sequences in `ZMod n`
+-/
+
+open Finset MvPolynomial
+open scoped BigOperators
+
+variable {ι : Type*}
+
+section prime
+variable {p : ℕ} [Fact p.Prime] {s : Finset ι}
+
+set_option linter.unusedVariables false in
+/-- The first multivariate polynomial used in the proof of Erdős–Ginzburg–Ziv. -/
+private noncomputable def f₁ (s : Finset ι) (a : ι → ZMod p) : MvPolynomial s (ZMod p) :=
+  ∑ i, X i ^ (p - 1)
+
+/-- The second multivariate polynomial used in the proof of Erdős–Ginzburg–Ziv. -/
+private noncomputable def f₂ (s : Finset ι) (a : ι → ZMod p) : MvPolynomial s (ZMod p) :=
+  ∑ i : s, a i • X i ^ (p - 1)
+
+private lemma totalDegree_f₁_add_totalDegree_f₂ {a : ι → ZMod p} :
+    (f₁ s a).totalDegree + (f₂ s a).totalDegree < 2 * p - 1 := by
+  calc
+    _ ≤ (p - 1) + (p - 1) := by
+      gcongr <;> apply totalDegree_finsetSum_le <;> rintro i _
+      · exact (totalDegree_X_pow ..).le
+      · exact (totalDegree_smul_le ..).trans (totalDegree_X_pow ..).le
+    _ < 2 * p - 1 := by have := (Fact.out : p.Prime).two_le; omega
+
+/-- The prime case of the **Erdős–Ginzburg–Ziv theorem** for `ℤ/pℤ`.
+
+Any sequence of `2 * p - 1` elements of `ZMod p` contains a subsequence of `p` elements whose sum is
+zero. -/
+private theorem ZMod.erdos_ginzburg_ziv_prime (a : ι → ZMod p) (hs : s.card = 2 * p - 1) :
+    ∃ t ⊆ s, t.card = p ∧ ∑ i ∈ t, a i = 0 := by
+  haveI : NeZero p := inferInstance
+  classical
+  -- Let `N` be the number of common roots of our polynomials `f₁` and `f₂` (`f s ff` and `f s tt`).
+  set N := Fintype.card {x // eval x (f₁ s a) = 0 ∧ eval x (f₂ s a) = 0}
+  -- Zero is a common root to `f₁` and `f₂`, so `N` is nonzero
+  let zero_sol : {x // eval x (f₁ s a) = 0 ∧ eval x (f₂ s a) = 0} :=
+    ⟨0, by simp [f₁, f₂, map_sum, (Fact.out : p.Prime).one_lt, tsub_eq_zero_iff_le]⟩
+  have hN₀ : 0 < N := @Fintype.card_pos _ _ ⟨zero_sol⟩
+  have hs' : 2 * p - 1 = Fintype.card s := by simp [hs]
+  -- Chevalley-Warning gives us that `p ∣ n` because the total degrees of `f₁` and `f₂` are at most
+  -- `p - 1`, and we have `2 * p - 1 > 2 * (p - 1)` variables.
+  have hpN : p ∣ N := char_dvd_card_solutions_of_add_lt p
+    (totalDegree_f₁_add_totalDegree_f₂.trans_eq hs')
+  -- Hence, `2 ≤ p ≤ N` and we can make a common root `x ≠ 0`.
+  obtain ⟨x, hx⟩ := Fintype.exists_ne_of_one_lt_card ((Fact.out : p.Prime).one_lt.trans_le $
+    Nat.le_of_dvd hN₀ hpN) zero_sol
+  -- This common root gives us the required subsequence, namely the `i ∈ s` such that `x i ≠ 0`.
+  refine ⟨(s.attach.filter fun a ↦ x.1 a ≠ 0).map ⟨(↑), Subtype.val_injective⟩, ?_, ?_, ?_⟩
+  · simp (config := { contextual := true }) [subset_iff]
+  -- From `f₁ x = 0`, we get that `p` divides the number of `a` such that `x a ≠ 0`.
+  · rw [card_map]
+    refine Nat.eq_of_dvd_of_lt_two_mul (Finset.card_pos.2 ?_).ne' ?_ $
+      (Finset.card_filter_le _ _).trans_lt ?_
+    -- This number is nonzero because `x ≠ 0`.
+    · rw [← Subtype.coe_ne_coe, Function.ne_iff] at hx
+      exact hx.imp (fun a ha ↦ mem_filter.2 ⟨Finset.mem_attach _ _, ha⟩)
+    · rw [← CharP.cast_eq_zero_iff (ZMod p), ← Finset.sum_boole]
+      simpa only [f₁, map_sum, ZMod.pow_card_sub_one, map_pow, eval_X] using x.2.1
+    -- And it is at most `2 * p - 1`, so it must be `p`.
+    · rw [Finset.card_attach, hs]
+      exact tsub_lt_self (mul_pos zero_lt_two (Fact.out : p.Prime).pos) zero_lt_one
+  -- From `f₂ x = 0`, we get that `p` divides the sum of the `a ∈ s` such that `x a ≠ 0`.
+  · simpa [f₂, ZMod.pow_card_sub_one, Finset.sum_filter] using x.2.2
+
+/-- The prime case of the **Erdős–Ginzburg–Ziv theorem** for `ℤ`.
+
+Any sequence of `2 * p - 1` elements of `ℤ` contains a subsequence of `p` elements whose sum is
+divisible by `p`. -/
+private theorem Int.erdos_ginzburg_ziv_prime (a : ι → ℤ) (hs : s.card = 2 * p - 1) :
+    ∃ t ⊆ s, t.card = p ∧ ↑p ∣ ∑ i ∈ t, a i := by
+  simpa [← Int.cast_sum, ZMod.intCast_zmod_eq_zero_iff_dvd]
+    using ZMod.erdos_ginzburg_ziv_prime (Int.cast ∘ a) hs
+
+end prime
+
+section composite
+variable {n : ℕ} {s : Finset ι}
+
+/-- The **Erdős–Ginzburg–Ziv theorem** for `ℤ`.
+
+Any sequence of at least `2 * n - 1` elements of `ℤ` contains a subsequence of `n` elements whose
+sum is divisible by `n`. -/
+theorem Int.erdos_ginzburg_ziv (a : ι → ℤ) (hs : 2 * n - 1 ≤ s.card) :
+    ∃ t ⊆ s, t.card = n ∧ ↑n ∣ ∑ i ∈ t, a i := by
+  classical
+  -- Do induction on the prime factorisation of `n`. Note that we will apply the induction
+  -- hypothesis with `ι := Finset ι`, so we need to generalise.
+  induction n using Nat.prime_composite_induction generalizing ι
+  -- When `n := 0`, we can set `t := ∅`.
+  case zero => exact ⟨∅, by simp⟩
+  -- When `n := 1`, we can take `t` to be any subset of `s` of size `2 * n - 1`.
+  case one => simpa using exists_subset_card_eq hs
+  -- When `n := p` is prime, we use the prime case `Int.erdos_ginzburg_ziv_prime`.
+  case prime p hp =>
+    haveI := Fact.mk hp
+    obtain ⟨t, hts, ht⟩ := exists_subset_card_eq hs
+    obtain ⟨u, hut, hu⟩ := Int.erdos_ginzburg_ziv_prime a ht
+    exact ⟨u, hut.trans hts, hu⟩
+  -- When `n := m * n` is composite, we pick (by induction hypothesis on `n`) `2 * m - 1` sets of
+  -- size `n` and sums divisible by `n`. Then by induction hypothesis (on `m`) we can pick `m` of
+  -- these sets whose sum is divisible by `m * n`.
+  case composite m hm ihm n hn ihn =>
+     -- First, show that it is enough to have those `2 * m - 1` sets.
+    suffices ∀ k ≤ 2 * m - 1, ∃ 𝒜 : Finset (Finset ι), 𝒜.card = k ∧
+      (𝒜 : Set (Finset ι)).Pairwise _root_.Disjoint ∧
+        ∀ ⦃t⦄, t ∈ 𝒜 → t ⊆ s ∧ t.card = n ∧ ↑n ∣ ∑ i ∈ t, a i by
+     -- Assume `𝒜` is a family of `2 * m - 1` sets, each of size `n` and sum divisible by `n`.
+      obtain ⟨𝒜, h𝒜card, h𝒜disj, h𝒜⟩ := this _ le_rfl
+      -- By induction hypothesis on `m`, find a subfamily `ℬ` of size `m` such that the sum over
+      -- `t ∈ ℬ` of `(∑ i ∈ t, a i) / n` is divisible by `m`.
+      obtain ⟨ℬ, hℬ𝒜, hℬcard, hℬ⟩ := ihm (fun t ↦ (∑ i ∈ t, a i) / n) h𝒜card.ge
+      -- We are done.
+      refine ⟨ℬ.biUnion fun x ↦ x, biUnion_subset.2 fun t ht ↦ (h𝒜 $ hℬ𝒜 ht).1, ?_, ?_⟩
+      · rw [card_biUnion (h𝒜disj.mono hℬ𝒜), sum_const_nat fun t ht ↦ (h𝒜 $ hℬ𝒜 ht).2.1, hℬcard]
+      rwa [sum_biUnion, natCast_mul, mul_comm, ← Int.dvd_div_iff_mul_dvd, Int.sum_div]
+      · exact fun t ht ↦ (h𝒜 $ hℬ𝒜 ht).2.2
+      · exact dvd_sum fun t ht ↦ (h𝒜 $ hℬ𝒜 ht).2.2
+      · exact h𝒜disj.mono hℬ𝒜
+    -- Now, let's find those `2 * m - 1` sets.
+    rintro k hk
+    -- We induct on the size `k ≤ 2 * m - 1` of the family we are constructing.
+    induction' k with k ih
+    -- For `k = 0`, the empty family trivially works.
+    · exact ⟨∅, by simp⟩
+    -- At `k + 1`, call `𝒜` the existing family of size `k ≤ 2 * m - 2`.
+    obtain ⟨𝒜, h𝒜card, h𝒜disj, h𝒜⟩ := ih (Nat.le_of_succ_le hk)
+    -- There are at least `2 * (m * n) - 1 - k * n ≥ 2 * m - 1` elements in `s` that have not been
+    -- taken in any element of `𝒜`.
+    have : 2 * n - 1 ≤ (s \ 𝒜.biUnion id).card := by
+      calc
+        _ ≤ (2 * m - k) * n - 1 := by gcongr; omega
+        _ = (2 * (m * n) - 1) - ∑ t ∈ 𝒜, t.card := by
+          rw [tsub_mul, mul_assoc, tsub_right_comm, sum_const_nat fun t ht ↦ (h𝒜 ht).2.1, h𝒜card]
+        _ ≤ s.card - (𝒜.biUnion id).card := by gcongr; exact card_biUnion_le
+        _ ≤ (s \ 𝒜.biUnion id).card := le_card_sdiff ..
+    -- So by the induction hypothesis on `n` we can find a new set `t` of size `n` and sum divisible
+    -- by `n`.
+    obtain ⟨t₀, ht₀, ht₀card, ht₀sum⟩ := ihn a this
+    -- This set is distinct and disjoint from the previous ones, so we are done.
+    have : t₀ ∉ 𝒜 := by
+      rintro h
+      obtain rfl : n = 0 := by
+        simpa [← card_eq_zero, ht₀card] using sdiff_disjoint.mono ht₀ $ subset_biUnion_of_mem id h
+      omega
+    refine ⟨𝒜.cons t₀ this, by rw [card_cons, h𝒜card], ?_, ?_⟩
+    · simp only [cons_eq_insert, coe_insert, Set.pairwise_insert_of_symmetric symmetric_disjoint,
+        mem_coe, ne_eq]
+      exact ⟨h𝒜disj, fun t ht _ ↦ sdiff_disjoint.mono ht₀ $ subset_biUnion_of_mem id ht⟩
+    · simp only [cons_eq_insert, mem_insert, forall_eq_or_imp, and_assoc]
+      exact ⟨ht₀.trans sdiff_subset, ht₀card, ht₀sum, h𝒜⟩
+
+/-- The **Erdős–Ginzburg–Ziv theorem** for `ℤ/nℤ`.
+
+Any sequence of at least `2 * n - 1` elements of `ZMod n` contains a subsequence of `n` elements
+whose sum is zero. -/
+theorem ZMod.erdos_ginzburg_ziv (a : ι → ZMod n) (hs : 2 * n - 1 ≤ s.card) :
+    ∃ t ⊆ s, t.card = n ∧ ∑ i ∈ t, a i = 0 := by
+  simpa [← ZMod.intCast_zmod_eq_zero_iff_dvd] using Int.erdos_ginzburg_ziv (ZMod.cast ∘ a) hs
+
+/-- The **Erdős–Ginzburg–Ziv theorem** for `ℤ` for multiset.
+
+Any multiset of at least `2 * n - 1` elements of `ℤ` contains a submultiset of `n` elements whose
+sum is divisible by `n`. -/
+theorem Int.erdos_ginzburg_ziv_multiset (s : Multiset ℤ) (hs : 2 * n - 1 ≤ Multiset.card s) :
+    ∃ t ≤ s, Multiset.card t = n ∧ ↑n ∣ t.sum := by
+  obtain ⟨t, hts, ht⟩ := Int.erdos_ginzburg_ziv (s := s.toEnumFinset) Prod.fst (by simpa using hs)
+  exact ⟨t.1.map Prod.fst, Multiset.map_fst_le_of_subset_toEnumFinset hts, by simpa using ht⟩
+
+/-- The **Erdős–Ginzburg–Ziv theorem** for `ℤ/nℤ` for multiset.
+
+Any multiset of at least `2 * n - 1` elements of `ℤ` contains a submultiset of `n` elements whose
+sum is divisible by `n`. -/
+theorem ZMod.erdos_ginzburg_ziv_multiset (s : Multiset (ZMod n))
+    (hs : 2 * n - 1 ≤ Multiset.card s) : ∃ t ≤ s, Multiset.card t = n ∧ t.sum = 0 := by
+  obtain ⟨t, hts, ht⟩ := ZMod.erdos_ginzburg_ziv (s := s.toEnumFinset) Prod.fst (by simpa using hs)
+  exact ⟨t.1.map Prod.fst, Multiset.map_fst_le_of_subset_toEnumFinset hts, by simpa using ht⟩
+
+end composite

Mathlib/Data/Multiset/Fintype.lean

@@ -103,6 +103,37 @@ theorem Multiset.mem_toEnumFinset (m : Multiset α) (p : α × ℕ) :
 theorem Multiset.mem_of_mem_toEnumFinset {p : α × ℕ} (h : p ∈ m.toEnumFinset) : p.1 ∈ m :=
   have := (m.mem_toEnumFinset p).mp h; Multiset.count_pos.mp (by omega)
 
+namespace Multiset
+
+@[simp] lemma toEnumFinset_filter_eq (m : Multiset α) (a : α) :
+    m.toEnumFinset.filter (·.1 = a) = {a} ×ˢ Finset.range (m.count a) := by aesop
+
+@[simp] lemma map_toEnumFinset_fst (m : Multiset α) : m.toEnumFinset.val.map Prod.fst = m := by
+  ext a; simp [count_map, ← Finset.filter_val, eq_comm (a := a)]
+
+@[simp] lemma image_toEnumFinset_fst (m : Multiset α) :
+    m.toEnumFinset.image Prod.fst = m.toFinset := by
+  rw [Finset.image, Multiset.map_toEnumFinset_fst]
+
+@[simp] lemma map_fst_le_of_subset_toEnumFinset {s : Finset (α × ℕ)} (hsm : s ⊆ m.toEnumFinset) :
+    s.1.map Prod.fst ≤ m := by
+  simp_rw [le_iff_count, count_map]
+  rintro a
+  obtain ha | ha := (s.1.filter fun x ↦ a = x.1).card.eq_zero_or_pos
+  · rw [ha]
+    exact Nat.zero_le _
+  obtain ⟨n, han, hn⟩ : ∃ n ≥ card (s.1.filter fun x ↦ a = x.1) - 1, (a, n) ∈ s := by
+    by_contra! h
+    replace h : s.filter (·.1 = a) ⊆ {a} ×ˢ .range (card (s.1.filter fun x ↦ a = x.1) - 1) := by
+      simpa (config := { contextual := true }) [forall_swap (β := _ = a), Finset.subset_iff,
+        imp_not_comm, not_le, Nat.lt_sub_iff_add_lt] using h
+    have : card (s.1.filter fun x ↦ a = x.1) ≤ card (s.1.filter fun x ↦ a = x.1) - 1 := by
+      simpa [Finset.card, eq_comm] using Finset.card_mono h
+    omega
+  exact Nat.le_of_pred_lt (han.trans_lt $ by simpa using hsm hn)
+
+end Multiset
+
 @[mono]
 theorem Multiset.toEnumFinset_mono {m₁ m₂ : Multiset α} (h : m₁ ≤ m₂) :
     m₁.toEnumFinset ⊆ m₂.toEnumFinset := by
@@ -112,17 +143,8 @@ theorem Multiset.toEnumFinset_mono {m₁ m₂ : Multiset α} (h : m₁ ≤ m₂)
 
 @[simp]
 theorem Multiset.toEnumFinset_subset_iff {m₁ m₂ : Multiset α} :
-    m₁.toEnumFinset ⊆ m₂.toEnumFinset ↔ m₁ ≤ m₂ := by
-  refine ⟨fun h ↦ ?_, Multiset.toEnumFinset_mono⟩
-  rw [Multiset.le_iff_count]
-  intro x
-  by_cases hx : x ∈ m₁
-  · apply Nat.le_of_pred_lt
-    have : (x, m₁.count x - 1) ∈ m₁.toEnumFinset := by
-      rw [Multiset.mem_toEnumFinset]
-      exact Nat.pred_lt (ne_of_gt (Multiset.count_pos.mpr hx))
-    simpa only [Multiset.mem_toEnumFinset] using h this
-  · simp [hx]
+    m₁.toEnumFinset ⊆ m₂.toEnumFinset ↔ m₁ ≤ m₂ :=
+  ⟨fun h ↦ by simpa using map_fst_le_of_subset_toEnumFinset h, Multiset.toEnumFinset_mono⟩
 
 /-- The embedding from a multiset into `α × ℕ` where the second coordinate enumerates repeats.
 If you are looking for the function `m → α`, that would be plain `(↑)`. -/
@@ -169,27 +191,6 @@ theorem Multiset.map_univ_coeEmbedding (m : Multiset α) :
     exists_prop, exists_eq_right_right, exists_eq_right, Multiset.mem_toEnumFinset, iff_self_iff,
     true_and_iff]
 
-theorem Multiset.toEnumFinset_filter_eq (m : Multiset α) (x : α) :
-    (m.toEnumFinset.filter fun p ↦ x = p.1) =
-      (Finset.range (m.count x)).map ⟨Prod.mk x, Prod.mk.inj_left x⟩ := by
-  ext ⟨y, i⟩
-  simp only [eq_comm, Finset.mem_filter, Multiset.mem_toEnumFinset, Finset.mem_map,
-    Finset.mem_range, Function.Embedding.coeFn_mk, Prod.mk.inj_iff, exists_prop,
-    exists_eq_right_right', and_congr_left_iff]
-  rintro rfl
-  rfl
-
-@[simp]
-theorem Multiset.map_toEnumFinset_fst (m : Multiset α) : m.toEnumFinset.val.map Prod.fst = m := by
-  ext x
-  simp only [Multiset.count_map, ← Finset.filter_val, Multiset.toEnumFinset_filter_eq,
-    Finset.map_val, Finset.range_val, Multiset.card_map, Multiset.card_range]
-
-@[simp]
-theorem Multiset.image_toEnumFinset_fst (m : Multiset α) :
-    m.toEnumFinset.image Prod.fst = m.toFinset := by
-  rw [Finset.image, Multiset.map_toEnumFinset_fst]
-
 @[simp]
 theorem Multiset.map_univ_coe (m : Multiset α) :
     (Finset.univ : Finset m).val.map (fun x : m ↦ (x : α)) = m := by

Mathlib/Data/Nat/Factorization/Induction.lean

@@ -74,8 +74,25 @@ def recOnMul {P : ℕ → Sort*} (h0 : P 0) (h1 : P 1) (hp : ∀ p, Prime p →
     | n + 1 => h _ _ (hp'' p n hp') (hp p hp')
   recOnPrimeCoprime h0 hp'' fun a b _ _ _ => h a b
 
-/-! ## Lemmas on multiplicative functions -/
+lemma _root_.induction_on_primes {P : ℕ → Prop} (h₀ : P 0) (h₁ : P 1)
+    (h : ∀ p a : ℕ, p.Prime → P a → P (p * a)) : ∀ n, P n := by
+  refine recOnPrimePow h₀ h₁ ?_
+  rintro a p n hp - - ha
+  induction' n with n ih
+  · simpa using ha
+  · rw [pow_succ', mul_assoc]
+    exact h _ _ hp ih
+
+lemma prime_composite_induction {P : ℕ → Prop} (zero : P 0) (one : P 1)
+    (prime : ∀ p : ℕ, p.Prime → P p) (composite : ∀ a, 2 ≤ a → P a → ∀ b, 2 ≤ b → P b → P (a * b))
+    (n : ℕ) : P n := by
+  refine induction_on_primes zero one ?_ _
+  rintro p (_ | _ | a) hp ha
+  · simpa
+  · simpa using prime _ hp
+  · exact composite _ hp.two_le (prime _ hp) _ a.one_lt_succ_succ ha
 
+/-! ## Lemmas on multiplicative functions -/
 
 /-- For any multiplicative function `f` with `f 1 = 1` and any `n ≠ 0`,
 we can evaluate `f n` by evaluating `f` at `p ^ k` over the factorization of `n` -/

Mathlib/RingTheory/UniqueFactorizationDomain.lean

@@ -1970,13 +1970,4 @@ lemma factors_multiset_prod_of_irreducible {s : Multiset ℕ} (h : ∀ x : ℕ,
   rw [Ne, Multiset.prod_eq_zero_iff]
   exact fun con ↦ not_irreducible_zero (h 0 con)
 
-lemma _root_.induction_on_primes {P : ℕ → Prop} (h₀ : P 0) (h₁ : P 1)
-    (h : ∀ p a : ℕ, p.Prime → P a → P (p * a)) (n : ℕ) : P n := by
-  apply UniqueFactorizationMonoid.induction_on_prime
-  · exact h₀
-  · intro n h
-    rw [Nat.isUnit_iff.1 h]
-    exact h₁
-  · exact fun a p _ hp ↦ h p a hp.nat_prime
-
 end Nat