Additional lemmas about elements of a ring satisfying IsCoprime

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

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

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

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

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

Alias of the forward direction of Nat.isCoprime_iff_coprime.

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

Alias of the reverse direction of Nat.isCoprime_iff_coprime.

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

theorem ne_zero_or_ne_zero_of_nat_coprime {A : Type u} [CommRing A] [Nontrivial A] {a : ℕ} {b : ℕ} (h : Nat.Coprime a 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} : (∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (Finset.prod t fun (i : I) => 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 (Finset.prod t fun (i : I) => s i)

theorem IsCoprime.prod_left_iff {R : Type u} {I : Type v} [CommSemiring R] {x : R} {s : I → R} {t : Finset I} : IsCoprime (Finset.prod t fun (i : I) => 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 (Finset.prod t fun (i : I) => 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 (Finset.prod t fun (i : I) => 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 (Finset.prod t fun (i : I) => 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} : Set.Pairwise (↑t) (IsCoprime on s) → (∀ i ∈ t, s i ∣ z) → (Finset.prod t fun (x : I) => 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 (IsCoprime on s)) (Hs1 : ∀ (i : I), s i ∣ z) : (Finset.prod Finset.univ fun (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), (Finset.sum t fun (i : I) => μ i * Finset.prod (t \ {i}) fun (j : I) => s j) = 1) ↔ Pairwise (IsCoprime on fun (i : { x : I // x ∈ 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), (Finset.sum Finset.univ fun (i : I) => μ i * Finset.prod {i}ᶜ fun (j : I) => s j) = 1) ↔ Pairwise (IsCoprime on s)

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) (Finset.prod (t \ {i}) fun (j : I) => s j)

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

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

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

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

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

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