Documentation

Mathlib.RingTheory.Coprime.Lemmas

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

Alias of the forward direction of Nat.isCoprime_iff_coprime.

theorem Nat.Coprime.isCoprime {m : } {n : } :
Nat.Coprime m 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 : 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 : IR} {t : Finset I} :
(it, 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 : IR} {t : Finset I} :
(it, 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 : IR} {t : Finset I} :
IsCoprime (Finset.prod t fun (i : I) => 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 (Finset.prod t fun (i : I) => 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 (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 : IR} {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 : IR} {t : Finset I} :
Set.Pairwise (t) (IsCoprime on s)(it, 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 : IR} [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 : IR} {t : Finset I} [DecidableEq I] (h : t.Nonempty) :
(∃ (μ : IR), (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 : IR} [Fintype I] [Nonempty I] [DecidableEq I] :
(∃ (μ : IR), (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 : IR} {t : Finset I} [DecidableEq I] :
Pairwise (IsCoprime on fun (i : { x : I // x t }) => s i) it, 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