Mathlib.RingTheory.Coprime.Lemmas

Int.isCoprime_iff_gcd_eq_one theorem

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

Full source

theorem Int.isCoprime_iff_gcd_eq_one {m n : ℤ} : IsCoprimeIsCoprime m n ↔ Int.gcd m n = 1 := by
  constructor
  · rintro ⟨a, b, h⟩
    refine Nat.dvd_one.mp (Int.gcd_dvd_iff.mpr ⟨a, b, ?_⟩)
    rwa [mul_comm m, mul_comm n, eq_comm]
  · rw [← Int.ofNat_inj, IsCoprime, Int.gcd_eq_gcd_ab, mul_comm m, mul_comm n, Nat.cast_one]
    intro h
    exact ⟨_, _, h⟩

Characterization of Coprime Integers via GCD: $\text{IsCoprime}(m, n) \leftrightarrow \gcd(m, n) = 1$

Informal description

For any integers $m$ and $n$, the elements $m$ and $n$ are coprime (i.e., $\text{IsCoprime}(m, n)$ holds) if and only if their greatest common divisor $\gcd(m, n)$ equals $1$.

Nat.isCoprime_iff_coprime theorem

{m n : ℕ} : IsCoprime (m : ℤ) n ↔ Nat.Coprime m n

Full source

theorem Nat.isCoprime_iff_coprime {m n : ℕ} : IsCoprimeIsCoprime (m : ℤ) n ↔ Nat.Coprime m n := by
  rw [Int.isCoprime_iff_gcd_eq_one, Int.gcd_natCast_natCast]

Equivalence of Coprimality in Natural Numbers and Their Integer Lifts: $\text{IsCoprime}(m, n) \leftrightarrow \text{Coprime}(m, n)$

Informal description

For any natural numbers $m$ and $n$, the elements $m$ and $n$ are coprime in the integers (i.e., $\text{IsCoprime}(m, n)$ holds) if and only if they are coprime in the natural numbers (i.e., $\text{Coprime}(m, n)$ holds).

Nat.Coprime.cast theorem

{R : Type*} [CommRing R] {a b : ℕ} (h : Nat.Coprime a b) : IsCoprime (a : R) (b : R)

Full source

theorem Nat.Coprime.cast {R : Type*} [CommRing R] {a b : ℕ} (h : Nat.Coprime a b) :
    IsCoprime (a : R) (b : R) := by
  rw [← isCoprime_iff_coprime] at h
  rw [← Int.cast_natCast a, ← Int.cast_natCast b]
  exact IsCoprime.intCast h

Preservation of Natural Number Coprimality under Ring Casting

Informal description

Let $R$ be a commutative ring. For any natural numbers $a$ and $b$ that are coprime (i.e., $\gcd(a, b) = 1$), their images under the canonical homomorphism from $\mathbb{N}$ to $R$ are also coprime in $R$.

ne_zero_or_ne_zero_of_nat_coprime theorem

{A : Type u} [CommRing A] [Nontrivial A] {a b : ℕ} (h : Nat.Coprime a b) : (a : A) ≠ 0 ∨ (b : A) ≠ 0

Full source

theorem ne_zero_or_ne_zero_of_nat_coprime {A : Type u} [CommRing A] [Nontrivial A] {a b : ℕ}
    (h : Nat.Coprime a b) : (a : A) ≠ 0(a : A) ≠ 0 ∨ (b : A) ≠ 0 :=
  IsCoprime.ne_zero_or_ne_zero (R := A) <| by
    simpa only [map_natCast] using IsCoprime.map (Nat.Coprime.isCoprime h) (Int.castRingHom A)

Nonzero Images of Coprime Natural Numbers in Nontrivial Commutative Rings

Informal description

Let $A$ be a nontrivial commutative ring. For any natural numbers $a$ and $b$ that are coprime, their images in $A$ satisfy $(a : A) \neq 0$ or $(b : A) \neq 0$.

IsCoprime.prod_left theorem

: (∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (∏ i ∈ t, s i) x

Full source

theorem IsCoprime.prod_left : (∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (∏ i ∈ t, s i) x := by
  classical
  refine Finset.induction_on t (fun _ ↦ isCoprime_one_left) fun b t hbt ih H ↦ ?_
  rw [Finset.prod_insert hbt]
  rw [Finset.forall_mem_insert] at H
  exact H.1.mul_left (ih H.2)

Coprimality of Product with Fixed Element

Informal description

For any finite set $t$ and any family of elements $(s_i)_{i \in t}$ in a ring or monoid, if each $s_i$ is coprime with a fixed element $x$, then the product $\prod_{i \in t} s_i$ is also coprime with $x$.

IsCoprime.prod_right theorem

: (∀ i ∈ t, IsCoprime x (s i)) → IsCoprime x (∏ i ∈ t, s i)

Full source

theorem IsCoprime.prod_right : (∀ i ∈ t, IsCoprime x (s i)) → IsCoprime x (∏ i ∈ t, s i) := by
  simpa only [isCoprime_comm] using IsCoprime.prod_left (R := R)

Coprimality of Fixed Element with Product

Informal description

For any finite set $t$ and any family of elements $(s_i)_{i \in t}$ in a ring or monoid, if a fixed element $x$ is coprime with each $s_i$, then $x$ is also coprime with the product $\prod_{i \in t} s_i$.

IsCoprime.prod_left_iff theorem

: IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x

Full source

theorem IsCoprime.prod_left_iff : IsCoprimeIsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x := by
  classical
  refine Finset.induction_on t (iff_of_true isCoprime_one_left fun _ ↦ by simp) fun b t hbt ih ↦ ?_
  rw [Finset.prod_insert hbt, IsCoprime.mul_left_iff, ih, Finset.forall_mem_insert]

Product Coprimality Criterion: $\prod_{i \in t} s_i \coprime x \leftrightarrow \forall i \in t, s_i \coprime x$

Informal description

For a finite set $t$ and a family of elements $(s_i)_{i \in t}$ in a ring or monoid, the product $\prod_{i \in t} s_i$ is coprime with an element $x$ if and only if each $s_i$ is coprime with $x$.

IsCoprime.prod_right_iff theorem

: IsCoprime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, IsCoprime x (s i)

Full source

theorem IsCoprime.prod_right_iff : IsCoprimeIsCoprime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, IsCoprime x (s i) := by
  simpa only [isCoprime_comm] using IsCoprime.prod_left_iff (R := R)

Product Coprimality Criterion: $x \coprime \prod_{i \in t} s_i \leftrightarrow \forall i \in t, x \coprime s_i$

Informal description

For a finite set $t$ and a family of elements $(s_i)_{i \in t}$ in a ring or monoid, an element $x$ is coprime with the product $\prod_{i \in t} s_i$ if and only if $x$ is coprime with each $s_i$ for all $i \in t$.

IsCoprime.of_prod_left theorem

(H1 : IsCoprime (∏ i ∈ t, s i) x) (i : I) (hit : i ∈ t) : IsCoprime (s i) x

Full source

theorem IsCoprime.of_prod_left (H1 : IsCoprime (∏ i ∈ t, s i) x) (i : I) (hit : i ∈ t) :
    IsCoprime (s i) x :=
  IsCoprime.prod_left_iff.1 H1 i hit

Coprimality of Factors Implies Coprimality of Product Elements

Informal description

Let $I$ be a type, $t$ be a finite subset of $I$, and $(s_i)_{i \in t}$ be a family of elements in a ring or monoid. If the product $\prod_{i \in t} s_i$ is coprime with an element $x$, then for any $i \in t$, the element $s_i$ is coprime with $x$.

IsCoprime.of_prod_right theorem

(H1 : IsCoprime x (∏ i ∈ t, s i)) (i : I) (hit : i ∈ t) : IsCoprime x (s i)

Full source

theorem IsCoprime.of_prod_right (H1 : IsCoprime x (∏ i ∈ t, s i)) (i : I) (hit : i ∈ t) :
    IsCoprime x (s i) :=
  IsCoprime.prod_right_iff.1 H1 i hit

Coprimality of Element with Product Implies Coprimality with Factors

Informal description

Let $I$ be a type, $t$ be a finite subset of $I$, and $(s_i)_{i \in t}$ be a family of elements in a ring or monoid. If an element $x$ is coprime with the product $\prod_{i \in t} s_i$, then for any $i \in t$, the element $x$ is coprime with $s_i$.

Finset.prod_dvd_of_coprime theorem

: (t : Set I).Pairwise (IsCoprime on s) → (∀ i ∈ t, s i ∣ z) → (∏ x ∈ t, s x) ∣ z

Full source

theorem Finset.prod_dvd_of_coprime :
    (t : Set I).Pairwise (IsCoprimeIsCoprime on s) → (∀ i ∈ t, s i ∣ z) → (∏ x ∈ t, s x) ∣ z := by
  classical
  exact Finset.induction_on t (fun _ _ ↦ one_dvd z)
    (by
      intro a r har ih Hs Hs1
      rw [Finset.prod_insert har]
      have aux1 : a ∈ (↑(insert a r) : Set I) := Finset.mem_insert_self a r
      refine
        (IsCoprime.prod_right fun i hir ↦
              Hs aux1 (Finset.mem_insert_of_mem hir) <| by
                rintro rfl
                exact har hir).mul_dvd
          (Hs1 a aux1) (ih (Hs.mono ?_) fun i hi ↦ Hs1 i <| Finset.mem_insert_of_mem hi)
      simp only [Finset.coe_insert, Set.subset_insert])

Product of Pairwise Coprime Elements Divides Common Multiple

Informal description

Let $I$ be a type, $t$ be a finite subset of $I$, and $s \colon I \to R$ be a family of elements in a ring $R$. If the elements $(s_i)_{i \in t}$ are pairwise coprime (i.e., $s_i$ and $s_j$ are coprime for all distinct $i, j \in t$) and each $s_i$ divides an element $z \in R$, then the product $\prod_{i \in t} s_i$ also divides $z$.

Fintype.prod_dvd_of_coprime theorem

[Fintype I] (Hs : Pairwise (IsCoprime on s)) (Hs1 : ∀ i, s i ∣ z) : (∏ x, s x) ∣ z

Full source

theorem Fintype.prod_dvd_of_coprime [Fintype I] (Hs : Pairwise (IsCoprimeIsCoprime on s))
    (Hs1 : ∀ i, s i ∣ z) : (∏ x, s x) ∣ z :=
  Finset.prod_dvd_of_coprime (Hs.set_pairwise _) fun i _ ↦ Hs1 i

Product of Pairwise Coprime Elements Divides Common Multiple (Finite Type Case)

Informal description

Let $I$ be a finite type and $s \colon I \to R$ a family of elements in a ring $R$. If the elements $(s_i)_{i \in I}$ are pairwise coprime (i.e., $s_i$ and $s_j$ are coprime for all distinct $i, j \in I$) and each $s_i$ divides an element $z \in R$, then the product $\prod_{i \in I} s_i$ also divides $z$.

exists_sum_eq_one_iff_pairwise_coprime theorem

 [DecidableEq I] (h : t.Nonempty) :
  (∃ μ : I → R, (∑ i ∈ t, μ i * ∏ j ∈ t \ { i }, s j) = 1) ↔ Pairwise (IsCoprime on fun i : t ↦ s i)

Full source

theorem exists_sum_eq_one_iff_pairwise_coprime [DecidableEq I] (h : t.Nonempty) :
    (∃ μ : I → R, (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) = 1) ↔
      Pairwise (IsCoprime on fun i : t ↦ s i) := by
  induction h using Finset.Nonempty.cons_induction with
  | singleton =>
    simp [exists_apply_eq, Pairwise, Function.onFun]
  | cons a t hat h ih =>
    rw [pairwise_cons']
    have mem : ∀ x ∈ t, a ∈ insert a t \ {x} := fun x hx ↦ by
      rw [mem_sdiff, mem_singleton]
      exact ⟨mem_insert_self _ _, fun ha ↦ hat (ha ▸ hx)⟩
    constructor
    · rintro ⟨μ, hμ⟩
      rw [sum_cons, cons_eq_insert, sdiff_singleton_eq_erase, erase_insert hat] at hμ
      refine ⟨ih.mp ⟨Pi.single h.choose (μ a * s h.choose) + μ * fun _ ↦ s a, ?_⟩, fun b hb ↦ ?_⟩
      · rw [prod_eq_mul_prod_diff_singleton h.choose_spec, ← mul_assoc, ←
          @if_pos _ _ h.choose_spec R (_ * _) 0, ← sum_pi_single', ← sum_add_distrib] at hμ
        rw [← hμ, sum_congr rfl]
        intro x hx
        dsimp -- Porting note: terms were showing as sort of `HAdd.hadd` instead of `+`
        -- this whole proof pretty much breaks and has to be rewritten from scratch
        rw [add_mul]
        congr 1
        · by_cases hx : x = h.choose
          · rw [hx, Pi.single_eq_same, Pi.single_eq_same]
          · rw [Pi.single_eq_of_ne hx, Pi.single_eq_of_ne hx, zero_mul]
        · rw [mul_assoc]
          congr
          rw [prod_eq_prod_diff_singleton_mul (mem x hx) _, mul_comm]
          congr 2
          rw [sdiff_sdiff_comm, sdiff_singleton_eq_erase a, erase_insert hat]
      · have : IsCoprime (s b) (s a) :=
          ⟨μ a * ∏ i ∈ t \ {b}, s i, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j, ?_⟩
        · exact ⟨this.symm, this⟩
        rw [mul_assoc, ← prod_eq_prod_diff_singleton_mul hb, sum_mul, ← hμ, sum_congr rfl]
        intro x hx
        rw [mul_assoc]
        congr
        rw [prod_eq_prod_diff_singleton_mul (mem x hx) _]
        congr 2
        rw [sdiff_sdiff_comm, sdiff_singleton_eq_erase a, erase_insert hat]
    · rintro ⟨hs, Hb⟩
      obtain ⟨μ, hμ⟩ := ih.mpr hs
      obtain ⟨u, v, huv⟩ := IsCoprime.prod_left fun b hb ↦ (Hb b hb).right
      use fun i ↦ if i = a then u else v * μ i
      have hμ' : (∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a)) = v * s a := by
        rw [← mul_sum, ← sum_mul, hμ, one_mul]
      rw [sum_cons, cons_eq_insert, sdiff_singleton_eq_erase, erase_insert hat]
      simp only [↓reduceIte, ite_mul]
      rw [← huv, ← hμ', sum_congr rfl]
      intro x hx
      rw [mul_assoc, if_neg fun ha : x = a ↦ hat (ha.casesOn hx)]
      rw [mul_assoc]
      congr
      rw [prod_eq_prod_diff_singleton_mul (mem x hx) _]
      congr 2
      rw [sdiff_sdiff_comm, sdiff_singleton_eq_erase a, erase_insert hat]

Existence of Bézout coefficients for pairwise coprime elements in a ring

Informal description

Let $I$ be a type with decidable equality, $t$ a nonempty finite subset of $I$, and $s : I \to R$ a family of elements in a ring $R$. Then there exists a family $\mu : I \to R$ such that \[ \sum_{i \in t} \mu_i \cdot \prod_{j \in t \setminus \{i\}} s_j = 1 \] if and only if the elements $(s_i)_{i \in t}$ are pairwise coprime (i.e., $s_i$ and $s_j$ are coprime for all distinct $i,j \in t$).

exists_sum_eq_one_iff_pairwise_coprime' theorem

 [Fintype I] [Nonempty I] [DecidableEq I] :
  (∃ μ : I → R, (∑ i : I, μ i * ∏ j ∈ { i }ᶜ, s j) = 1) ↔ Pairwise (IsCoprime on s)

Full source

theorem exists_sum_eq_one_iff_pairwise_coprime' [Fintype I] [Nonempty I] [DecidableEq I] :
    (∃ μ : I → R, (∑ i : I, μ i * ∏ j ∈ {i}ᶜ, s j) = 1) ↔ Pairwise (IsCoprime on s) := by
  convert exists_sum_eq_one_iff_pairwise_coprime Finset.univ_nonempty (s := s) using 1
  simp only [Function.onFun, pairwise_subtype_iff_pairwise_finset', coe_univ, Set.pairwise_univ]

Existence of Bézout coefficients for pairwise coprime elements in a finite ring

Informal description

Let $I$ be a finite nonempty type with decidable equality, and let $s : I \to R$ be a family of elements in a ring $R$. Then there exists a family $\mu : I \to R$ such that \[ \sum_{i \in I} \mu_i \cdot \prod_{j \neq i} s_j = 1 \] if and only if the elements $(s_i)_{i \in I}$ are pairwise coprime (i.e., $s_i$ and $s_j$ are coprime for all distinct $i,j \in I$).

pairwise_coprime_iff_coprime_prod theorem

[DecidableEq I] : Pairwise (IsCoprime on fun i : t ↦ s i) ↔ ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ { i }, s j)

Full source

theorem pairwise_coprime_iff_coprime_prod [DecidableEq I] :
    PairwisePairwise (IsCoprime on fun i : t ↦ s i) ↔ ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j) := by
  refine ⟨fun hp i hi ↦ IsCoprime.prod_right_iff.mpr fun j hj ↦ ?_, fun hp ↦ ?_⟩
  · rw [Finset.mem_sdiff, Finset.mem_singleton] at hj
    obtain ⟨hj, ji⟩ := hj
    refine @hp ⟨i, hi⟩ ⟨j, hj⟩ fun h ↦ ji (congrArg Subtype.val h).symm
    -- Porting note: is there a better way compared to the old `congr_arg coe h`?
  · rintro ⟨i, hi⟩ ⟨j, hj⟩ h
    apply IsCoprime.prod_right_iff.mp (hp i hi)
    exact Finset.mem_sdiff.mpr ⟨hj, fun f ↦ h <| Subtype.ext (Finset.mem_singleton.mp f).symm⟩

Pairwise Coprimality Criterion: $\text{Pairwise}(\coprime) \leftrightarrow \forall i \in t, s_i \coprime \prod_{j \neq i} s_j$

Informal description

For a finite set $t$ and a family of elements $(s_i)_{i \in t}$ in a ring or monoid, the following are equivalent: 1. The elements $(s_i)_{i \in t}$ are pairwise coprime (i.e., $s_i$ and $s_j$ are coprime for all distinct $i,j \in t$). 2. For every $i \in t$, the element $s_i$ is coprime with the product $\prod_{j \in t \setminus \{i\}} s_j$.

IsCoprime.pow_left theorem

(H : IsCoprime x y) : IsCoprime (x ^ m) y

Full source

theorem IsCoprime.pow_left (H : IsCoprime x y) : IsCoprime (x ^ m) y := by
  rw [← Finset.card_range m, ← Finset.prod_const]
  exact IsCoprime.prod_left fun _ _ ↦ H

Coprimality is preserved under taking powers in the first argument

Informal description

If two elements $x$ and $y$ in a ring or monoid are coprime, then for any natural number $m$, the element $x^m$ is also coprime with $y$.

IsCoprime.pow_right theorem

(H : IsCoprime x y) : IsCoprime x (y ^ n)

Full source

theorem IsCoprime.pow_right (H : IsCoprime x y) : IsCoprime x (y ^ n) := by
  rw [← Finset.card_range n, ← Finset.prod_const]
  exact IsCoprime.prod_right fun _ _ ↦ H

Coprimality is preserved under taking powers in the second argument

Informal description

If two elements $x$ and $y$ in a ring or monoid are coprime, then for any natural number $n$, the element $x$ is coprime with $y^n$.

IsCoprime.pow theorem

(H : IsCoprime x y) : IsCoprime (x ^ m) (y ^ n)

Full source

theorem IsCoprime.pow (H : IsCoprime x y) : IsCoprime (x ^ m) (y ^ n) :=
  H.pow_left.pow_right

Coprimality is preserved under taking powers in both arguments

Informal description

If two elements $x$ and $y$ in a ring or monoid are coprime, then for any natural numbers $m$ and $n$, the elements $x^m$ and $y^n$ are also coprime.

IsCoprime.pow_left_iff theorem

(hm : 0 < m) : IsCoprime (x ^ m) y ↔ IsCoprime x y

Full source

theorem IsCoprime.pow_left_iff (hm : 0 < m) : IsCoprimeIsCoprime (x ^ m) y ↔ IsCoprime x y := by
  refine ⟨fun h ↦ ?_, IsCoprime.pow_left⟩
  rw [← Finset.card_range m, ← Finset.prod_const] at h
  exact h.of_prod_left 0 (Finset.mem_range.mpr hm)

Coprimality of Powers: $x^m$ and $y$ are coprime iff $x$ and $y$ are coprime for $m > 0$

Informal description

For any positive integer $m$, the elements $x^m$ and $y$ in a ring or monoid are coprime if and only if $x$ and $y$ are coprime.

IsCoprime.pow_right_iff theorem

(hm : 0 < m) : IsCoprime x (y ^ m) ↔ IsCoprime x y

Full source

theorem IsCoprime.pow_right_iff (hm : 0 < m) : IsCoprimeIsCoprime x (y ^ m) ↔ IsCoprime x y :=
  isCoprime_comm.trans <| (IsCoprime.pow_left_iff hm).trans <| isCoprime_comm

Coprimality of Powers: $x \coprime y^m \leftrightarrow x \coprime y$ for $m > 0$

Informal description

For any positive integer $m$, the elements $x$ and $y^m$ in a ring or monoid are coprime if and only if $x$ and $y$ are coprime.

IsCoprime.pow_iff theorem

(hm : 0 < m) (hn : 0 < n) : IsCoprime (x ^ m) (y ^ n) ↔ IsCoprime x y

Full source

theorem IsCoprime.pow_iff (hm : 0 < m) (hn : 0 < n) : IsCoprimeIsCoprime (x ^ m) (y ^ n) ↔ IsCoprime x y :=
  (IsCoprime.pow_left_iff hm).trans <| IsCoprime.pow_right_iff hn

Coprimality of Powers: $x^m \coprime y^n \leftrightarrow x \coprime y$ for $m, n > 0$

Informal description

For any positive integers $m$ and $n$, the elements $x^m$ and $y^n$ in a ring or monoid are coprime if and only if $x$ and $y$ are coprime.

IsRelPrime.prod_left theorem

: (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x

Full source

theorem IsRelPrime.prod_left : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x := by
  classical
  refine Finset.induction_on t (fun _ ↦ isRelPrime_one_left) fun b t hbt ih H ↦ ?_
  rw [Finset.prod_insert hbt]
  rw [Finset.forall_mem_insert] at H
  exact H.1.mul_left (ih H.2)

Product of Relatively Prime Elements is Relatively Prime

Informal description

For a family of elements $(s_i)_{i \in t}$ in a monoid and an element $x$, if each $s_i$ is relatively prime to $x$ for all $i \in t$, then the product $\prod_{i \in t} s_i$ is also relatively prime to $x$.

IsRelPrime.prod_right theorem

: (∀ i ∈ t, IsRelPrime x (s i)) → IsRelPrime x (∏ i ∈ t, s i)

Full source

theorem IsRelPrime.prod_right : (∀ i ∈ t, IsRelPrime x (s i)) → IsRelPrime x (∏ i ∈ t, s i) := by
  simpa only [isRelPrime_comm] using IsRelPrime.prod_left (α := α)

Right Product of Relatively Prime Elements is Relatively Prime

Informal description

For a family of elements $(s_i)_{i \in t}$ in a monoid and an element $x$, if $x$ is relatively prime to each $s_i$ for all $i \in t$, then $x$ is also relatively prime to the product $\prod_{i \in t} s_i$.

IsRelPrime.prod_left_iff theorem

: IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x

Full source

theorem IsRelPrime.prod_left_iff : IsRelPrimeIsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x := by
  classical
  refine Finset.induction_on t (iff_of_true isRelPrime_one_left fun _ ↦ by simp) fun b t hbt ih ↦ ?_
  rw [Finset.prod_insert hbt, IsRelPrime.mul_left_iff, ih, Finset.forall_mem_insert]

Product of Elements is Relatively Prime to $x$ if and only if Each Element is Relatively Prime to $x$

Informal description

For a family of elements $(s_i)_{i \in t}$ in a monoid and an element $x$, the product $\prod_{i \in t} s_i$ is relatively prime to $x$ if and only if each $s_i$ is relatively prime to $x$ for all $i \in t$.

IsRelPrime.prod_right_iff theorem

: IsRelPrime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, IsRelPrime x (s i)

Full source

theorem IsRelPrime.prod_right_iff : IsRelPrimeIsRelPrime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, IsRelPrime x (s i) := by
  simpa only [isRelPrime_comm] using IsRelPrime.prod_left_iff (α := α)

$x$ is Relatively Prime to a Product if and only if it is Relatively Prime to Each Factor

Informal description

For a family of elements $(s_i)_{i \in t}$ in a monoid and an element $x$, the element $x$ is relatively prime to the product $\prod_{i \in t} s_i$ if and only if $x$ is relatively prime to each $s_i$ for all $i \in t$.

IsRelPrime.of_prod_left theorem

(H1 : IsRelPrime (∏ i ∈ t, s i) x) (i : I) (hit : i ∈ t) : IsRelPrime (s i) x

Full source

theorem IsRelPrime.of_prod_left (H1 : IsRelPrime (∏ i ∈ t, s i) x) (i : I) (hit : i ∈ t) :
    IsRelPrime (s i) x :=
  IsRelPrime.prod_left_iff.1 H1 i hit

Relative Primeness of Factors Implies Relative Primeness of Product

Informal description

Let $(s_i)_{i \in t}$ be a family of elements in a monoid and $x$ be another element. If the product $\prod_{i \in t} s_i$ is relatively prime to $x$, then for any index $i \in t$, the element $s_i$ is relatively prime to $x$.

IsRelPrime.of_prod_right theorem

(H1 : IsRelPrime x (∏ i ∈ t, s i)) (i : I) (hit : i ∈ t) : IsRelPrime x (s i)

Full source

theorem IsRelPrime.of_prod_right (H1 : IsRelPrime x (∏ i ∈ t, s i)) (i : I) (hit : i ∈ t) :
    IsRelPrime x (s i) :=
  IsRelPrime.prod_right_iff.1 H1 i hit

Relative Primeness to Product Implies Relative Primeness to Each Factor

Informal description

Let $(s_i)_{i \in t}$ be a family of elements in a monoid and $x$ be another element. If $x$ is relatively prime to the product $\prod_{i \in t} s_i$, then for any index $i \in t$, the element $x$ is relatively prime to $s_i$.

Finset.prod_dvd_of_isRelPrime theorem

: (t : Set I).Pairwise (IsRelPrime on s) → (∀ i ∈ t, s i ∣ z) → (∏ x ∈ t, s x) ∣ z

Full source

theorem Finset.prod_dvd_of_isRelPrime :
    (t : Set I).Pairwise (IsRelPrimeIsRelPrime on s) → (∀ i ∈ t, s i ∣ z) → (∏ x ∈ t, s x) ∣ z := by
  classical
  exact Finset.induction_on t (fun _ _ ↦ one_dvd z)
    (by
      intro a r har ih Hs Hs1
      rw [Finset.prod_insert har]
      have aux1 : a ∈ (↑(insert a r) : Set I) := Finset.mem_insert_self a r
      refine
        (IsRelPrime.prod_right fun i hir ↦
              Hs aux1 (Finset.mem_insert_of_mem hir) <| by
                rintro rfl
                exact har hir).mul_dvd
          (Hs1 a aux1) (ih (Hs.mono ?_) fun i hi ↦ Hs1 i <| Finset.mem_insert_of_mem hi)
      simp only [Finset.coe_insert, Set.subset_insert])

Product of Pairwise Relatively Prime Elements Divides Common Multiple

Informal description

Let $I$ be a type, $t$ be a set of indices in $I$, and $(s_i)_{i \in t}$ be a family of elements in a monoid. If the elements $s_i$ are pairwise relatively prime (i.e., any two distinct elements in $t$ are relatively prime) and each $s_i$ divides an element $z$, then the product $\prod_{i \in t} s_i$ divides $z$.

Fintype.prod_dvd_of_isRelPrime theorem

[Fintype I] (Hs : Pairwise (IsRelPrime on s)) (Hs1 : ∀ i, s i ∣ z) : (∏ x, s x) ∣ z

Full source

theorem Fintype.prod_dvd_of_isRelPrime [Fintype I] (Hs : Pairwise (IsRelPrimeIsRelPrime on s))
    (Hs1 : ∀ i, s i ∣ z) : (∏ x, s x) ∣ z :=
  Finset.prod_dvd_of_isRelPrime (Hs.set_pairwise _) fun i _ ↦ Hs1 i

Product of Pairwise Relatively Prime Elements Divides Common Multiple in Finite Case

Informal description

Let $I$ be a finite type, $(s_i)_{i \in I}$ be a family of elements in a monoid, and $z$ be another element. If the elements $s_i$ are pairwise relatively prime and each $s_i$ divides $z$, then the product $\prod_{i \in I} s_i$ divides $z$.

pairwise_isRelPrime_iff_isRelPrime_prod theorem

 [DecidableEq I] : Pairwise (IsRelPrime on fun i : t ↦ s i) ↔ ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ { i }, s j)

Full source

theorem pairwise_isRelPrime_iff_isRelPrime_prod [DecidableEq I] :
    PairwisePairwise (IsRelPrime on fun i : t ↦ s i) ↔ ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j) := by
  refine ⟨fun hp i hi ↦ IsRelPrime.prod_right_iff.mpr fun j hj ↦ ?_, fun hp ↦ ?_⟩
  · rw [Finset.mem_sdiff, Finset.mem_singleton] at hj
    obtain ⟨hj, ji⟩ := hj
    exact @hp ⟨i, hi⟩ ⟨j, hj⟩ fun h ↦ ji (congrArg Subtype.val h).symm
  · rintro ⟨i, hi⟩ ⟨j, hj⟩ h
    apply IsRelPrime.prod_right_iff.mp (hp i hi)
    exact Finset.mem_sdiff.mpr ⟨hj, fun f ↦ h <| Subtype.ext (Finset.mem_singleton.mp f).symm⟩

Pairwise Relative Primality is Equivalent to Relative Primality with Product of Complements

Informal description

For a finite set $t$ with decidable equality and a family of elements $(s_i)_{i \in t}$ in a monoid, the following are equivalent: 1. The elements $s_i$ are pairwise relatively prime. 2. For every $i \in t$, the element $s_i$ is relatively prime to the product $\prod_{j \in t \setminus \{i\}} s_j$.

IsRelPrime.pow_left theorem

(H : IsRelPrime x y) : IsRelPrime (x ^ m) y

Full source

theorem pow_left (H : IsRelPrime x y) : IsRelPrime (x ^ m) y := by
  rw [← Finset.card_range m, ← Finset.prod_const]
  exact IsRelPrime.prod_left fun _ _ ↦ H

Relatively Prime Elements Remain So Under Powers: $x^m$ and $y$

Informal description

If two elements $x$ and $y$ in a monoid are relatively prime, then for any natural number $m$, the element $x^m$ is also relatively prime to $y$.

IsRelPrime.pow_right theorem

(H : IsRelPrime x y) : IsRelPrime x (y ^ n)

Full source

theorem pow_right (H : IsRelPrime x y) : IsRelPrime x (y ^ n) := by
  rw [← Finset.card_range n, ← Finset.prod_const]
  exact IsRelPrime.prod_right fun _ _ ↦ H

Relatively Prime Elements Remain So Under Powers: $x$ and $y^n$

Informal description

If two elements $x$ and $y$ in a monoid are relatively prime, then for any natural number $n$, the element $x$ is also relatively prime to $y^n$.

IsRelPrime.pow theorem

(H : IsRelPrime x y) : IsRelPrime (x ^ m) (y ^ n)

Full source

theorem pow (H : IsRelPrime x y) : IsRelPrime (x ^ m) (y ^ n) :=
  H.pow_left.pow_right

Relatively Prime Elements Remain So Under Powers: $x^m$ and $y^n$

Informal description

If two elements $x$ and $y$ in a monoid are relatively prime, then for any natural numbers $m$ and $n$, the elements $x^m$ and $y^n$ are also relatively prime.

IsRelPrime.pow_left_iff theorem

(hm : 0 < m) : IsRelPrime (x ^ m) y ↔ IsRelPrime x y

Full source

theorem pow_left_iff (hm : 0 < m) : IsRelPrimeIsRelPrime (x ^ m) y ↔ IsRelPrime x y := by
  refine ⟨fun h ↦ ?_, IsRelPrime.pow_left⟩
  rw [← Finset.card_range m, ← Finset.prod_const] at h
  exact h.of_prod_left 0 (Finset.mem_range.mpr hm)

Equivalence of Relative Primeness Under Powers: $x^m$ and $y$ iff $x$ and $y$

Informal description

For any elements $x$ and $y$ in a monoid and any positive integer $m$, the element $x^m$ is relatively prime to $y$ if and only if $x$ is relatively prime to $y$. In other words, $$ \text{IsRelPrime}(x^m, y) \leftrightarrow \text{IsRelPrime}(x, y). $$

IsRelPrime.pow_right_iff theorem

(hm : 0 < m) : IsRelPrime x (y ^ m) ↔ IsRelPrime x y

Full source

theorem pow_right_iff (hm : 0 < m) : IsRelPrimeIsRelPrime x (y ^ m) ↔ IsRelPrime x y :=
  isRelPrime_comm.trans <| (IsRelPrime.pow_left_iff hm).trans <| isRelPrime_comm

Equivalence of Relative Primeness Under Powers: $x$ and $y^m$ iff $x$ and $y$

Informal description

For any elements $x$ and $y$ in a monoid and any positive integer $m$, the element $x$ is relatively prime to $y^m$ if and only if $x$ is relatively prime to $y$. In other words, $$ \text{IsRelPrime}(x, y^m) \leftrightarrow \text{IsRelPrime}(x, y). $$

IsRelPrime.pow_iff theorem

(hm : 0 < m) (hn : 0 < n) : IsRelPrime (x ^ m) (y ^ n) ↔ IsRelPrime x y

Full source

theorem pow_iff (hm : 0 < m) (hn : 0 < n) :
    IsRelPrimeIsRelPrime (x ^ m) (y ^ n) ↔ IsRelPrime x y :=
  (IsRelPrime.pow_left_iff hm).trans (IsRelPrime.pow_right_iff hn)

Equivalence of Relative Primeness Under Powers: $x^m$ and $y^n$ iff $x$ and $y$

Informal description

For any elements $x$ and $y$ in a monoid and any positive integers $m$ and $n$, the element $x^m$ is relatively prime to $y^n$ if and only if $x$ is relatively prime to $y$. In other words, $$ \text{IsRelPrime}(x^m, y^n) \leftrightarrow \text{IsRelPrime}(x, y). $$