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 HasPow since these are easiest to prove via Finset.prod.
Alias of the forward direction of Nat.isCoprime_iff_coprime.
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)
:
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]
:
theorem
IsCoprime.pow_left
{R : Type u}
[CommSemiring R]
{x : R}
{y : R}
{m : ℕ}
(H : IsCoprime x y)
:
theorem
IsCoprime.pow_right
{R : Type u}
[CommSemiring R]
{x : R}
{y : R}
{n : ℕ}
(H : IsCoprime x y)
:
theorem
IsCoprime.pow
{R : Type u}
[CommSemiring R]
{x : R}
{y : R}
{m : ℕ}
{n : ℕ}
(H : IsCoprime x y)
:
theorem
IsCoprime.pow_right_iff
{R : Type u}
[CommSemiring R]
{x : R}
{y : R}
{m : ℕ}
(hm : 0 < m)
:
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 (Finset.prod t fun (i : I) => 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 (Finset.prod t fun (i : I) => s i)
theorem
IsRelPrime.prod_left_iff
{α : Type u_1}
{I : Type u_2}
[CommMonoid α]
[DecompositionMonoid α]
{x : α}
{s : I → α}
{t : Finset I}
:
IsRelPrime (Finset.prod t fun (i : I) => 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 (Finset.prod t fun (i : I) => 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 (Finset.prod t fun (i : I) => 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 (Finset.prod t fun (i : I) => 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}
:
Set.Pairwise (↑t) (IsRelPrime on s) → (∀ i ∈ t, s i ∣ z) → (Finset.prod t fun (x : I) => 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 (IsRelPrime on s))
(Hs1 : ∀ (i : I), s i ∣ z)
:
(Finset.prod Finset.univ fun (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 (IsRelPrime on fun (i : { x : I // x ∈ t }) => s ↑i) ↔ ∀ i ∈ t, IsRelPrime (s i) (Finset.prod (t \ {i}) fun (j : 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