Documentation

Mathlib.RingTheory.Coprime.Lemmas

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
theorem Nat.isCoprime_iff_coprime {m : } {n : } :
IsCoprime m n m.Coprime n
theorem IsCoprime.nat_coprime {m : } {n : } :
IsCoprime m nm.Coprime n

Alias of the forward direction of Nat.isCoprime_iff_coprime.

theorem Nat.Coprime.isCoprime {m : } {n : } :
m.Coprime nIsCoprime 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 : a.Coprime b) :
IsCoprime a b
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 : IR} {t : Finset I} :
(∀ it, IsCoprime (s i) x)IsCoprime (∏ it, s i) x
theorem IsCoprime.prod_right {R : Type u} {I : Type v} [CommSemiring R] {x : R} {s : IR} {t : Finset I} :
(∀ it, IsCoprime x (s i))IsCoprime x (∏ it, s i)
theorem IsCoprime.prod_left_iff {R : Type u} {I : Type v} [CommSemiring R] {x : R} {s : IR} {t : Finset I} :
IsCoprime (∏ it, s i) x it, IsCoprime (s i) x
theorem IsCoprime.prod_right_iff {R : Type u} {I : Type v} [CommSemiring R] {x : R} {s : IR} {t : Finset I} :
IsCoprime x (∏ it, s i) it, IsCoprime x (s i)
theorem IsCoprime.of_prod_left {R : Type u} {I : Type v} [CommSemiring R] {x : R} {s : IR} {t : Finset I} (H1 : IsCoprime (∏ it, 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 : IR} {t : Finset I} (H1 : IsCoprime x (∏ it, 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 : IR} {t : Finset I} :
(↑t).Pairwise (IsCoprime on s)(∀ it, s i z)xt, s x z
theorem Fintype.prod_dvd_of_coprime {R : Type u} {I : Type v} [CommSemiring R] {z : R} {s : IR} [Fintype I] (Hs : Pairwise (IsCoprime on 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 : IR} {t : Finset I} [DecidableEq I] (h : t.Nonempty) :
(∃ (μ : IR), it, μ i * jt \ {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 : IR} [Fintype I] [Nonempty I] [DecidableEq I] :
(∃ (μ : IR), i : I, μ i * j{i}, s j = 1) Pairwise (IsCoprime on s)
theorem pairwise_coprime_iff_coprime_prod {R : Type u} {I : Type v} [CommSemiring R] {s : IR} {t : Finset I} [DecidableEq I] :
Pairwise (IsCoprime on fun (i : { x : I // x t }) => s i) it, IsCoprime (s i) (∏ jt \ {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
theorem IsRelPrime.prod_left {α : Type u_2} {I : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x : α} {s : Iα} {t : Finset I} :
(∀ it, IsRelPrime (s i) x)IsRelPrime (∏ it, s i) x
theorem IsRelPrime.prod_right {α : Type u_2} {I : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x : α} {s : Iα} {t : Finset I} :
(∀ it, IsRelPrime x (s i))IsRelPrime x (∏ it, s i)
theorem IsRelPrime.prod_left_iff {α : Type u_1} {I : Type u_2} [CommMonoid α] [DecompositionMonoid α] {x : α} {s : Iα} {t : Finset I} :
IsRelPrime (∏ it, s i) x it, 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 (∏ it, s i) it, 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 (∏ it, 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 (∏ it, 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 (IsRelPrime on s)(∀ it, s i z)xt, 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) :
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) it, IsRelPrime (s i) (∏ jt \ {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) :
theorem IsRelPrime.pow_right_iff {α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x : α} {y : α} {m : } (hm : 0 < m) :
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