Documentation

Mathlib.RingTheory.Coprime.Lemmas

Additional lemmas about elements of a ring satisfying IsCoprime #

and elements of a monoid satisfying IsRelPrime

These lemmas are in a separate file to the definition of IsCoprime or IsRelPrime as they require more imports.

Notably, this includes lemmas about Finset.prod as this requires importing BigOperators, and lemmas about Pow since these are easiest to prove via Finset.prod.

source
theorem Int.isCoprime_iff_gcd_eq_one {m : ℤ} {n : ℤ} :
IsCoprime m n ↔ m.gcd n = 1
source
theorem Nat.isCoprime_iff_coprime {m : ℕ} {n : ℕ} :
IsCoprime ↑m ↑n ↔ m.Coprime n
source
theorem IsCoprime.nat_coprime {m : ℕ} {n : ℕ} :
IsCoprime ↑m ↑n → m.Coprime n

Alias of the forward direction of Nat.isCoprime_iff_coprime.

source
theorem Nat.Coprime.isCoprime {m : ℕ} {n : ℕ} :
m.Coprime n → IsCoprime ↑m ↑n

Alias of the reverse direction of Nat.isCoprime_iff_coprime.

source
theorem Nat.Coprime.cast {R : Type u_1} [CommRing R] {a : ℕ} {b : ℕ} (h : a.Coprime b) :
IsCoprime ↑a ↑b
source
theorem ne_zero_or_ne_zero_of_nat_coprime {A : Type u} [CommRing A] [Nontrivial A] {a : ℕ} {b : ℕ} (h : a.Coprime b) :
↑a ≠ 0 ∨ ↑b ≠ 0
source
theorem IsCoprime.prod_left {R : Type u} {I : Type v} [CommSemiring R] {x : R} {s : I → R} {t : Finset I} :
(∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (t.prod fun (i : I) => s i) x
source
theorem IsCoprime.prod_right {R : Type u} {I : Type v} [CommSemiring R] {x : R} {s : I → R} {t : Finset I} :
(∀ i ∈ t, IsCoprime x (s i)) → IsCoprime x (t.prod fun (i : I) => s i)
source
theorem IsCoprime.prod_left_iff {R : Type u} {I : Type v} [CommSemiring R] {x : R} {s : I → R} {t : Finset I} :
IsCoprime (t.prod fun (i : I) => s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x
source
theorem IsCoprime.prod_right_iff {R : Type u} {I : Type v} [CommSemiring R] {x : R} {s : I → R} {t : Finset I} :
IsCoprime x (t.prod fun (i : I) => s i) ↔ ∀ i ∈ t, IsCoprime x (s i)
source
theorem IsCoprime.of_prod_left {R : Type u} {I : Type v} [CommSemiring R] {x : R} {s : I → R} {t : Finset I} (H1 : IsCoprime (t.prod fun (i : I) => s i) x) (i : I) (hit : i ∈ t) :
IsCoprime (s i) x
source
theorem IsCoprime.of_prod_right {R : Type u} {I : Type v} [CommSemiring R] {x : R} {s : I → R} {t : Finset I} (H1 : IsCoprime x (t.prod fun (i : I) => s i)) (i : I) (hit : i ∈ t) :
IsCoprime x (s i)
source
theorem Finset.prod_dvd_of_coprime {R : Type u} {I : Type v} [CommSemiring R] {z : R} {s : I → R} {t : Finset I} :
(↑t).Pairwise (IsCoprime on s) → (∀ i ∈ t, s i ∣ z) → (t.prod fun (x : I) => s x) ∣ z
source
theorem Fintype.prod_dvd_of_coprime {R : Type u} {I : Type v} [CommSemiring R] {z : R} {s : I → R} [Fintype I] (Hs : Pairwise (IsCoprime on s)) (Hs1 : ∀ (i : I), s i ∣ z) :
(Finset.univ.prod fun (x : I) => s x) ∣ z
source
theorem exists_sum_eq_one_iff_pairwise_coprime {R : Type u} {I : Type v} [CommSemiring R] {s : I → R} {t : Finset I} [DecidableEq I] (h : t.Nonempty) :
(∃ (μ : I → R), (t.sum fun (i : I) => μ i * (t \ {i}).prod fun (j : I) => s j) = 1) ↔ Pairwise (IsCoprime on fun (i : { x : I // x ∈ t }) => s ↑i)
source
theorem exists_sum_eq_one_iff_pairwise_coprime' {R : Type u} {I : Type v} [CommSemiring R] {s : I → R} [Fintype I] [Nonempty I] [DecidableEq I] :
(∃ (μ : I → R), (Finset.univ.sum fun (i : I) => μ i * {i}ᶜ.prod fun (j : I) => s j) = 1) ↔ Pairwise (IsCoprime on s)
source
theorem pairwise_coprime_iff_coprime_prod {R : Type u} {I : Type v} [CommSemiring R] {s : I → R} {t : Finset I} [DecidableEq I] :
Pairwise (IsCoprime on fun (i : { x : I // x ∈ t }) => s ↑i) ↔ ∀ i ∈ t, IsCoprime (s i) ((t \ {i}).prod fun (j : I) => s j)
source
theorem IsCoprime.pow_left {R : Type u} [CommSemiring R] {x : R} {y : R} {m : ℕ} (H : IsCoprime x y) :
IsCoprime (x ^ m) y
source
theorem IsCoprime.pow_right {R : Type u} [CommSemiring R] {x : R} {y : R} {n : ℕ} (H : IsCoprime x y) :
IsCoprime x (y ^ n)
source
theorem IsCoprime.pow {R : Type u} [CommSemiring R] {x : R} {y : R} {m : ℕ} {n : ℕ} (H : IsCoprime x y) :
IsCoprime (x ^ m) (y ^ n)
source
theorem IsCoprime.pow_left_iff {R : Type u} [CommSemiring R] {x : R} {y : R} {m : ℕ} (hm : 0 < m) :
IsCoprime (x ^ m) y ↔ IsCoprime x y
source
theorem IsCoprime.pow_right_iff {R : Type u} [CommSemiring R] {x : R} {y : R} {m : ℕ} (hm : 0 < m) :
IsCoprime x (y ^ m) ↔ IsCoprime x y
source
theorem IsCoprime.pow_iff {R : Type u} [CommSemiring R] {x : R} {y : R} {m : ℕ} {n : ℕ} (hm : 0 < m) (hn : 0 < n) :
IsCoprime (x ^ m) (y ^ n) ↔ IsCoprime x y
source
theorem IsRelPrime.prod_left {α : Type u_2} {I : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x : α} {s : I → α} {t : Finset I} :
(∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (t.prod fun (i : I) => s i) x
source
theorem IsRelPrime.prod_right {α : Type u_2} {I : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x : α} {s : I → α} {t : Finset I} :
(∀ i ∈ t, IsRelPrime x (s i)) → IsRelPrime x (t.prod fun (i : I) => s i)
source
theorem IsRelPrime.prod_left_iff {α : Type u_1} {I : Type u_2} [CommMonoid α] [DecompositionMonoid α] {x : α} {s : I → α} {t : Finset I} :
IsRelPrime (t.prod fun (i : I) => s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x
source
theorem IsRelPrime.prod_right_iff {α : Type u_1} {I : Type u_2} [CommMonoid α] [DecompositionMonoid α] {x : α} {s : I → α} {t : Finset I} :
IsRelPrime x (t.prod fun (i : I) => s i) ↔ ∀ i ∈ t, IsRelPrime x (s i)
source
theorem IsRelPrime.of_prod_left {α : Type u_1} {I : Type u_2} [CommMonoid α] [DecompositionMonoid α] {x : α} {s : I → α} {t : Finset I} (H1 : IsRelPrime (t.prod fun (i : I) => s i) x) (i : I) (hit : i ∈ t) :
IsRelPrime (s i) x
source
theorem IsRelPrime.of_prod_right {α : Type u_1} {I : Type u_2} [CommMonoid α] [DecompositionMonoid α] {x : α} {s : I → α} {t : Finset I} (H1 : IsRelPrime x (t.prod fun (i : I) => s i)) (i : I) (hit : i ∈ t) :
IsRelPrime x (s i)
source
theorem Finset.prod_dvd_of_isRelPrime {α : Type u_2} {I : Type u_1} [CommMonoid α] [DecompositionMonoid α] {z : α} {s : I → α} {t : Finset I} :
(↑t).Pairwise (IsRelPrime on s) → (∀ i ∈ t, s i ∣ z) → (t.prod fun (x : I) => s x) ∣ z
source
theorem Fintype.prod_dvd_of_isRelPrime {α : Type u_2} {I : Type u_1} [CommMonoid α] [DecompositionMonoid α] {z : α} {s : I → α} [Fintype I] (Hs : Pairwise (IsRelPrime on s)) (Hs1 : ∀ (i : I), s i ∣ z) :
(Finset.univ.prod fun (x : I) => s x) ∣ z
source
theorem pairwise_isRelPrime_iff_isRelPrime_prod {α : Type u_2} {I : Type u_1} [CommMonoid α] [DecompositionMonoid α] {s : I → α} {t : Finset I} [DecidableEq I] :
Pairwise (IsRelPrime on fun (i : { x : I // x ∈ t }) => s ↑i) ↔ ∀ i ∈ t, IsRelPrime (s i) ((t \ {i}).prod fun (j : I) => s j)
source
theorem IsRelPrime.pow_left {α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x : α} {y : α} {m : ℕ} (H : IsRelPrime x y) :
IsRelPrime (x ^ m) y
source
theorem IsRelPrime.pow_right {α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x : α} {y : α} {n : ℕ} (H : IsRelPrime x y) :
IsRelPrime x (y ^ n)
source
theorem IsRelPrime.pow {α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x : α} {y : α} {m : ℕ} {n : ℕ} (H : IsRelPrime x y) :
IsRelPrime (x ^ m) (y ^ n)
source
theorem IsRelPrime.pow_left_iff {α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x : α} {y : α} {m : ℕ} (hm : 0 < m) :
IsRelPrime (x ^ m) y ↔ IsRelPrime x y
source
theorem IsRelPrime.pow_right_iff {α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x : α} {y : α} {m : ℕ} (hm : 0 < m) :
IsRelPrime x (y ^ m) ↔ IsRelPrime x y
source
theorem IsRelPrime.pow_iff {α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x : α} {y : α} {m : ℕ} {n : ℕ} (hm : 0 < m) (hn : 0 < n) :
IsRelPrime (x ^ m) (y ^ n) ↔ IsRelPrime x y