# 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
instance instDecidableRelIntIsCoprime :
DecidableRel IsCoprime
Equations

- instDecidableRelIntIsCoprime m n = decidable_of_iff (m.gcd n = 1) ⋯

source
@[simp]
theorem Nat.isCoprime_iff_coprime {m n : ℕ} :
IsCoprime ↑m ↑n ↔ m.Coprime n
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 IsCoprime.natCoprime {m n : ℕ} :
IsCoprime ↑m ↑n → m.Coprime n

Alias of the forward direction of `Nat.isCoprime_iff_coprime`.

source
@[deprecated IsCoprime.natCoprime (since := "2025-08-25")]
theorem IsCoprime.nat_coprime {m n : ℕ} :
IsCoprime ↑m ↑n → m.Coprime n

Alias of the forward direction of `Nat.isCoprime_iff_coprime`.

Alias of the forward 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} (h : ∀ i ∈ t, IsCoprime (s i) x) :
IsCoprime (∏ i ∈ t, 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 (∏ i ∈ t, 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 (∏ i ∈ t, 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 (∏ i ∈ t, 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 (∏ i ∈ t, 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 (∏ i ∈ t, 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} (Hs : (↑t).Pairwise (Function.onFun IsCoprime s)) (Hs1 : ∀ i ∈ t, s i ∣ z) :
∏ x ∈ t, 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 (Function.onFun IsCoprime s)) (Hs1 : ∀ (i : I), s i ∣ z) :
∏ 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), ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (Function.onFun IsCoprime fun (i : ↥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), ∑ i : I, μ i * ∏ j ∈ {i}ᶜ, s j = 1) ↔ Pairwise (Function.onFun IsCoprime 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 (Function.onFun IsCoprime fun (i : ↥t) => s ↑i) ↔ ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)
source
theorem IsCoprime.pow_left {R : Type u} [CommSemiring R] {x y : R} {m : ℕ} (H : IsCoprime x y) :
IsCoprime (x ^ m) y
source
theorem IsCoprime.pow_right {R : Type u} [CommSemiring R] {x y : R} {n : ℕ} (H : IsCoprime x y) :
IsCoprime x (y ^ n)
source
theorem IsCoprime.pow {R : Type u} [CommSemiring R] {x 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 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 y : R} {m : ℕ} (hm : 0 < m) :
IsCoprime x (y ^ m) ↔ IsCoprime x y
source
theorem IsCoprime.pow_iff {R : Type u} [CommSemiring R] {x 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 (∏ i ∈ t, 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 (∏ i ∈ t, s i)
source
theorem IsRelPrime.prod_left_iff {α : Type u_1} {I : Type u_2} [CommMonoid α] [DecompositionMonoid α] {x : α} {s : I → α} {t : Finset I} :
IsRelPrime (∏ i ∈ t, 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 (∏ i ∈ t, 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 (∏ i ∈ t, 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 (∏ i ∈ t, 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 (Function.onFun IsRelPrime s) → (∀ i ∈ t, s i ∣ z) → ∏ x ∈ t, 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 (Function.onFun IsRelPrime s)) (Hs1 : ∀ (i : I), s i ∣ z) :
∏ 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 (Function.onFun IsRelPrime fun (i : ↥t) => s ↑i) ↔ ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {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