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.

theorem Int.isCoprime_iff_gcd_eq_one {m n : ℤ} : IsCoprime m n ↔ m.gcd n = 1

instance instDecidableRelIntIsCoprime : DecidableRel IsCoprime

@[simp]

theorem Nat.isCoprime_iff_coprime {m n : ℕ} : IsCoprime ↑m ↑n ↔ m.Coprime n

theorem IsCoprime.natCoprime {m n : ℕ} : IsCoprime ↑m ↑n → m.Coprime n

Alias of the forward direction of Nat.isCoprime_iff_coprime.

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

Alias of the reverse direction of Nat.isCoprime_iff_coprime.

@[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.

theorem Nat.Coprime.cast {R : Type u_1} [CommRing R] {a b : ℕ} (h : a.Coprime b) : IsCoprime ↑a ↑b

theorem Rat.isCoprime_num_den (x : ℚ) : IsCoprime x.num ↑x.den

theorem Int.isCoprime_gcdA {x y : ℤ} (h : IsCoprime x y) : IsCoprime (x.gcdA y) y

theorem Int.isCoprime_gcdB {x y : ℤ} (h : IsCoprime x y) : IsCoprime (x.gcdB y) x

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

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

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)

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

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)

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

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)

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

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

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)

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)

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)

theorem IsCoprime.pow_left {R : Type u} [CommSemiring R] {x y : R} {m : ℕ} (H : IsCoprime x y) : IsCoprime (x ^ m) y

theorem IsCoprime.pow_right {R : Type u} [CommSemiring R] {x y : R} {n : ℕ} (H : IsCoprime x y) : IsCoprime x (y ^ n)

theorem IsCoprime.pow {R : Type u} [CommSemiring R] {x y : R} {m n : ℕ} (H : IsCoprime x y) : IsCoprime (x ^ m) (y ^ n)

theorem IsCoprime.pow_left_iff {R : Type u} [CommSemiring R] {x y : R} {m : ℕ} (hm : 0 < m) : IsCoprime (x ^ m) y ↔ IsCoprime x y

theorem IsCoprime.pow_right_iff {R : Type u} [CommSemiring R] {x y : R} {m : ℕ} (hm : 0 < m) : IsCoprime x (y ^ m) ↔ IsCoprime x y

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

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

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)

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

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)

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

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)

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

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

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)

theorem IsRelPrime.pow_left {α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x y : α} {m : ℕ} (H : IsRelPrime x y) : IsRelPrime (x ^ m) y

theorem IsRelPrime.pow_right {α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x y : α} {n : ℕ} (H : IsRelPrime x y) : IsRelPrime x (y ^ n)

theorem IsRelPrime.pow {α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x y : α} {m n : ℕ} (H : IsRelPrime x y) : IsRelPrime (x ^ m) (y ^ n)

theorem IsRelPrime.pow_left_iff {α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x y : α} {m : ℕ} (hm : 0 < m) : IsRelPrime (x ^ m) y ↔ IsRelPrime x y

theorem IsRelPrime.pow_right_iff {α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x y : α} {m : ℕ} (hm : 0 < m) : IsRelPrime x (y ^ m) ↔ IsRelPrime x y

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