From 3bd2044b1a23157374a81d1f561c0c7991ddad3a Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed, 5 Jan 2022 14:15:34 +0000 Subject: [PATCH] chore(data/nat/prime): reuse a result from algebra.big_operators.associated (#11143) --- src/algebra/big_operators/associated.lean | 23 ------- src/data/list/prime.lean | 82 +++++++++++++++++++++++ src/data/nat/prime.lean | 71 ++++---------------- 3 files changed, 95 insertions(+), 81 deletions(-) create mode 100644 src/data/list/prime.lean diff --git a/src/algebra/big_operators/associated.lean b/src/algebra/big_operators/associated.lean index 58f7e058cd0ab..024927f067eaf 100644 --- a/src/algebra/big_operators/associated.lean +++ b/src/algebra/big_operators/associated.lean @@ -135,27 +135,4 @@ lemma prime.dvd_finsupp_prod_iff {f: α →₀ M} {g : α → M → ℕ} {p : p ∣ f.prod g ↔ ∃ a ∈ f.support, p ∣ g a (f a) := prime.dvd_finset_prod_iff pp _ -/-- Prime `p` divides the product of a list `L` iff it divides some `a ∈ L` -/ -lemma prime.dvd_prod_iff {p : M} {L : list M} (pp : prime p) : -p ∣ L.prod ↔ ∃ a ∈ L, p ∣ a := -begin - split, - { intros h, - induction L, - { simp only [list.prod_nil] at h, exact absurd h (prime.not_dvd_one pp) }, - { rw list.prod_cons at h, - cases (prime.dvd_or_dvd pp) h, { use L_hd, simp [h_1] }, - { rcases L_ih h_1 with ⟨x, hx1, hx2⟩, use x, simp [list.mem_cons_iff, hx1, hx2] } } }, - { exact λ ⟨a, ha1, ha2⟩, dvd_trans ha2 (list.dvd_prod ha1) }, -end - end comm_monoid_with_zero - -lemma nat.prime.dvd_finset_prod_iff {α : Type*} {S : finset α} {p : ℕ} - (pp : prime p) (g : α → ℕ) : p ∣ S.prod g ↔ ∃ a ∈ S, p ∣ g a := -by apply prime.dvd_finset_prod_iff pp - -lemma nat.prime.dvd_finsupp_prod_iff {α M : Type*} [has_zero M] {f: α →₀ M} - {g : α → M → ℕ} {p : ℕ} (pp : prime p) : -p ∣ f.prod g ↔ ∃ a ∈ f.support, p ∣ g a (f a) := -nat.prime.dvd_finset_prod_iff pp _ diff --git a/src/data/list/prime.lean b/src/data/list/prime.lean new file mode 100644 index 0000000000000..bf6c5986e54c9 --- /dev/null +++ b/src/data/list/prime.lean @@ -0,0 +1,82 @@ +/- +Copyright (c) 2018 Johannes Hölzl. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johannes Hölzl, Jens Wagemaker, Anne Baanen +-/ + +import algebra.associated +import data.list.big_operators +import data.list.perm + +/-! +# Products of lists of prime elements. + +This file contains some theorems relating `prime` and products of `list`s. + +-/ + +open list + +section comm_monoid_with_zero + +variables {M : Type*} [comm_monoid_with_zero M] + +/-- Prime `p` divides the product of a list `L` iff it divides some `a ∈ L` -/ +lemma prime.dvd_prod_iff {p : M} {L : list M} (pp : prime p) : p ∣ L.prod ↔ ∃ a ∈ L, p ∣ a := +begin + split, + { intros h, + induction L with L_hd L_tl L_ih, + { rw prod_nil at h, exact absurd h pp.not_dvd_one }, + { rw prod_cons at h, + cases pp.dvd_or_dvd h with hd hd, + { exact ⟨L_hd, mem_cons_self L_hd L_tl, hd⟩ }, + { obtain ⟨x, hx1, hx2⟩ := L_ih hd, + exact ⟨x, mem_cons_of_mem L_hd hx1, hx2⟩ } } }, + { exact λ ⟨a, ha1, ha2⟩, dvd_trans ha2 (dvd_prod ha1) }, +end + +lemma prime.not_dvd_prod {p : M} {L : list M} (pp : prime p) (hL : ∀ a ∈ L, ¬ p ∣ a) : + ¬ p ∣ L.prod := +mt (prime.dvd_prod_iff pp).mp $ not_bex.mpr hL + +end comm_monoid_with_zero + +section cancel_comm_monoid_with_zero + +variables {M : Type*} [cancel_comm_monoid_with_zero M] [unique (units M)] + +lemma prime_dvd_prime_iff_eq {p q : M} (pp : prime p) (qp : prime q) : p ∣ q ↔ p = q := +by rw [pp.dvd_prime_iff_associated qp, ←associated_eq_eq] + +lemma mem_list_primes_of_dvd_prod {p : M} (hp : prime p) {L : list M} (hL : ∀ q ∈ L, prime q) + (hpL : p ∣ L.prod) : p ∈ L := +begin + obtain ⟨x, hx1, hx2⟩ := hp.dvd_prod_iff.mp hpL, + rwa (prime_dvd_prime_iff_eq hp (hL x hx1)).mp hx2 +end + +lemma perm_of_prod_eq_prod : ∀ {l₁ l₂ : list M}, l₁.prod = l₂.prod → + (∀ p ∈ l₁, prime p) → (∀ p ∈ l₂, prime p) → perm l₁ l₂ +| [] [] _ _ _ := perm.nil +| [] (a :: l) h₁ h₂ h₃ := + have ha : a ∣ 1 := @prod_nil M _ ▸ h₁.symm ▸ (@prod_cons _ _ l a).symm ▸ dvd_mul_right _ _, + absurd ha (prime.not_dvd_one (h₃ a (mem_cons_self _ _))) +| (a :: l) [] h₁ h₂ h₃ := + have ha : a ∣ 1 := @prod_nil M _ ▸ h₁ ▸ (@prod_cons _ _ l a).symm ▸ dvd_mul_right _ _, + absurd ha (prime.not_dvd_one (h₂ a (mem_cons_self _ _))) +| (a :: l₁) (b :: l₂) h hl₁ hl₂ := + begin + classical, + have hl₁' : ∀ p ∈ l₁, prime p := λ p hp, hl₁ p (mem_cons_of_mem _ hp), + have hl₂' : ∀ p ∈ (b :: l₂).erase a, prime p := λ p hp, hl₂ p (mem_of_mem_erase hp), + have ha : a ∈ (b :: l₂) := mem_list_primes_of_dvd_prod (hl₁ a (mem_cons_self _ _)) hl₂ + (h ▸ by rw prod_cons; exact dvd_mul_right _ _), + have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha, + have hl : prod l₁ = prod ((b :: l₂).erase a) := + ((mul_right_inj' (hl₁ a (mem_cons_self _ _)).ne_zero).1 $ + by rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]), + exact perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm + end + +end cancel_comm_monoid_with_zero diff --git a/src/data/nat/prime.lean b/src/data/nat/prime.lean index be3ec47510600..aae4608f72c3e 100644 --- a/src/data/nat/prime.lean +++ b/src/data/nat/prime.lean @@ -3,7 +3,7 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro -/ -import algebra.associated +import data.list.prime import data.list.sort import data.nat.gcd import data.nat.sqrt @@ -538,28 +538,6 @@ theorem prime_iff {p : ℕ} : p.prime ↔ _root_.prime p := theorem irreducible_iff_prime {p : ℕ} : irreducible p ↔ _root_.prime p := by rw [←prime_iff, prime] -/-- Prime `p` divides the product of `L : list ℕ` iff it divides some `a ∈ L` -/ -lemma prime.dvd_prod_iff {p : ℕ} {L : list ℕ} (pp : p.prime) : - p ∣ L.prod ↔ ∃ a ∈ L, p ∣ a := -begin - split, - { intros h, - induction L, - { simp only [list.prod_nil] at h, exact absurd h (prime.not_dvd_one pp) }, - { rw list.prod_cons at h, - cases (prime.dvd_mul pp).mp h, - { use L_hd, simp [h_1] }, - { rcases L_ih h_1 with ⟨x, hx1, hx2⟩, use x, simp [list.mem_cons_iff, hx1, hx2] } } }, - { exact λ ⟨a, ha1, ha2⟩, dvd_trans ha2 (list.dvd_prod ha1) }, -end --- TODO: This proof duplicates a more general proof in `algebra/associated`. --- The two proofs should be integrated after the merger of `nat.prime` and `prime` --- that's about to occur. (2021-12-17) - -lemma prime.not_dvd_prod {p : ℕ} {L : list ℕ} (pp : prime p) (hL : ∀ a ∈ L, ¬ p ∣ a) : - ¬ p ∣ L.prod := -mt (prime.dvd_prod_iff pp).mp (not_bex.mpr hL) - theorem prime.dvd_of_dvd_pow {p m n : ℕ} (pp : prime p) (h : p ∣ m^n) : p ∣ m := begin induction n with n IH, @@ -723,17 +701,12 @@ by simpa using not_iff_not.mpr ne_one_iff_exists_prime_dvd section open list -lemma mem_list_primes_of_dvd_prod {p : ℕ} (hp : prime p) : - ∀ {l : list ℕ}, (∀ p ∈ l, prime p) → p ∣ prod l → p ∈ l := -begin - intros L hL hpL, - rcases (prime.dvd_prod_iff hp).mp hpL with ⟨x, hx1, hx2⟩, - rwa ((prime_dvd_prime_iff_eq hp (hL x hx1)).mp hx2) -end - lemma mem_factors_iff_dvd {n p : ℕ} (hn : 0 < n) (hp : prime p) : p ∈ factors n ↔ p ∣ n := ⟨λ h, prod_factors hn ▸ list.dvd_prod h, - λ h, mem_list_primes_of_dvd_prod hp (@prime_of_mem_factors n) ((prod_factors hn).symm ▸ h)⟩ + λ h, mem_list_primes_of_dvd_prod + (prime_iff.mp hp) + (λ p h, prime_iff.mp (prime_of_mem_factors h)) + ((prod_factors hn).symm ▸ h)⟩ lemma dvd_of_mem_factors {n p : ℕ} (h : p ∈ n.factors) : p ∣ n := begin @@ -746,36 +719,18 @@ lemma mem_factors {n p} (hn : 0 < n) : p ∈ factors n ↔ prime p ∧ p ∣ n : ⟨λ h, ⟨prime_of_mem_factors h, (mem_factors_iff_dvd hn $ prime_of_mem_factors h).mp h⟩, λ ⟨hprime, hdvd⟩, (mem_factors_iff_dvd hn hprime).mpr hdvd⟩ -lemma perm_of_prod_eq_prod : ∀ {l₁ l₂ : list ℕ}, prod l₁ = prod l₂ → - (∀ p ∈ l₁, prime p) → (∀ p ∈ l₂, prime p) → l₁ ~ l₂ -| [] [] _ _ _ := perm.nil -| [] (a :: l) h₁ h₂ h₃ := - have ha : a ∣ 1 := @prod_nil ℕ _ ▸ h₁.symm ▸ (@prod_cons _ _ l a).symm ▸ dvd_mul_right _ _, - absurd ha (prime.not_dvd_one (h₃ a (mem_cons_self _ _))) -| (a :: l) [] h₁ h₂ h₃ := - have ha : a ∣ 1 := @prod_nil ℕ _ ▸ h₁ ▸ (@prod_cons _ _ l a).symm ▸ dvd_mul_right _ _, - absurd ha (prime.not_dvd_one (h₂ a (mem_cons_self _ _))) -| (a :: l₁) (b :: l₂) h hl₁ hl₂ := - have hl₁' : ∀ p ∈ l₁, prime p := λ p hp, hl₁ p (mem_cons_of_mem _ hp), - have hl₂' : ∀ p ∈ (b :: l₂).erase a, prime p := λ p hp, hl₂ p (mem_of_mem_erase hp), - have ha : a ∈ (b :: l₂) := mem_list_primes_of_dvd_prod (hl₁ a (mem_cons_self _ _)) hl₂ - (h ▸ by rw prod_cons; exact dvd_mul_right _ _), - have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha, - have hl : prod l₁ = prod ((b :: l₂).erase a) := - (nat.mul_right_inj (prime.pos (hl₁ a (mem_cons_self _ _)))).1 $ - by rwa [← prod_cons, ← prod_cons, ← hb.prod_eq], - perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm - /-- **Fundamental theorem of arithmetic**-/ lemma factors_unique {n : ℕ} {l : list ℕ} (h₁ : prod l = n) (h₂ : ∀ p ∈ l, prime p) : l ~ factors n := begin - refine perm_of_prod_eq_prod _ h₂ (λ p, prime_of_mem_factors), - rw h₁, - refine (prod_factors (nat.pos_of_ne_zero _)).symm, - rintro rfl, - rw prod_eq_zero_iff at h₁, - exact prime.ne_zero (h₂ 0 h₁) rfl, + refine perm_of_prod_eq_prod _ _ _, + { rw h₁, + refine (prod_factors (nat.pos_of_ne_zero _)).symm, + rintro rfl, + rw prod_eq_zero_iff at h₁, + exact prime.ne_zero (h₂ 0 h₁) rfl }, + { simp_rw ←prime_iff, exact h₂ }, + { simp_rw ←prime_iff, exact (λ p, prime_of_mem_factors) }, end lemma prime.factors_pow {p : ℕ} (hp : p.prime) (n : ℕ) :