-
Notifications
You must be signed in to change notification settings - Fork 258
/
BigOperators.lean
62 lines (44 loc) · 2.41 KB
/
BigOperators.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
/-
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Leonardo de Moura
-/
import Mathlib.Algebra.BigOperators.Basic
#align_import data.nat.gcd.big_operators from "leanprover-community/mathlib"@"008205aa645b3f194c1da47025c5f110c8406eab"
/-! # Lemmas about coprimality with big products.
These lemmas are kept separate from `Data.Nat.GCD.Basic` in order to minimize imports.
-/
namespace Nat
open BigOperators
variable {ι : Type*}
theorem coprime_list_prod_left_iff {l : List ℕ} {k : ℕ} :
Coprime l.prod k ↔ ∀ n ∈ l, Coprime n k := by
induction l <;> simp [Nat.coprime_mul_iff_left, *]
theorem coprime_list_prod_right_iff {k : ℕ} {l : List ℕ} :
Coprime k l.prod ↔ ∀ n ∈ l, Coprime k n := by
simp_rw [coprime_comm (n := k), coprime_list_prod_left_iff]
theorem coprime_multiset_prod_left_iff {m : Multiset ℕ} {k : ℕ} :
Coprime m.prod k ↔ ∀ n ∈ m, Coprime n k := by
induction m using Quotient.inductionOn; simpa using coprime_list_prod_left_iff
theorem coprime_multiset_prod_right_iff {k : ℕ} {m : Multiset ℕ} :
Coprime k m.prod ↔ ∀ n ∈ m, Coprime k n := by
induction m using Quotient.inductionOn; simpa using coprime_list_prod_right_iff
theorem coprime_prod_left_iff {t : Finset ι} {s : ι → ℕ} {x : ℕ} :
Coprime (∏ i in t, s i) x ↔ ∀ i ∈ t, Coprime (s i) x := by
simpa using coprime_multiset_prod_left_iff (m := t.val.map s)
theorem coprime_prod_right_iff {x : ℕ} {t : Finset ι} {s : ι → ℕ} :
Coprime x (∏ i in t, s i) ↔ ∀ i ∈ t, Coprime x (s i) := by
simpa using coprime_multiset_prod_right_iff (m := t.val.map s)
/-- See `IsCoprime.prod_left` for the corresponding lemma about `IsCoprime` -/
alias ⟨_, Coprime.prod_left⟩ := coprime_prod_left_iff
#align nat.coprime_prod_left Nat.Coprime.prod_left
/-- See `IsCoprime.prod_right` for the corresponding lemma about `IsCoprime` -/
alias ⟨_, Coprime.prod_right⟩ := coprime_prod_right_iff
#align nat.coprime_prod_right Nat.Coprime.prod_right
theorem coprime_fintype_prod_left_iff [Fintype ι] {s : ι → ℕ} {x : ℕ} :
Coprime (∏ i, s i) x ↔ ∀ i, Coprime (s i) x := by
simp [coprime_prod_left_iff]
theorem coprime_fintype_prod_right_iff [Fintype ι] {x : ℕ} {s : ι → ℕ} :
Coprime x (∏ i, s i) ↔ ∀ i, Coprime x (s i) := by
simp [coprime_prod_right_iff]
end Nat