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 : Int} : Iff (IsCoprime m n) (Eq (m.gcd n) 1)

theorem Nat.isCoprime_iff_coprime {m n : Nat} : Iff (IsCoprime m.cast n.cast) (m.Coprime n)

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

Alias of the forward direction of Nat.isCoprime_iff_coprime.

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

Alias of the reverse direction of Nat.isCoprime_iff_coprime.

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

theorem ne_zero_or_ne_zero_of_nat_coprime {A : Type u} [CommRing A] [Nontrivial A] {a b : Nat} (h : a.Coprime b) : Or (Ne a.cast 0) (Ne b.cast 0)

theorem IsCoprime.prod_left {R : Type u} {I : Type v} [CommSemiring R] {x : R} {s : I → R} {t : Finset I} : (∀ (i : I), Membership.mem t i → IsCoprime (s i) x) → IsCoprime (t.prod 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 : I), Membership.mem t i → IsCoprime x (s i)) → IsCoprime x (t.prod 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} : Iff (IsCoprime (t.prod fun (i : I) => s i) x) (∀ (i : I), Membership.mem t i → 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} : Iff (IsCoprime x (t.prod fun (i : I) => s i)) (∀ (i : I), Membership.mem t i → 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 (t.prod fun (i : I) => s i) x) (i : I) (hit : Membership.mem t i) : 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 (t.prod fun (i : I) => s i)) (i : I) (hit : Membership.mem t i) : 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} : t.toSet.Pairwise (Function.onFun IsCoprime s) → (∀ (i : I), Membership.mem t i → Dvd.dvd (s i) z) → Dvd.dvd (t.prod 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 (Function.onFun IsCoprime s)) (Hs1 : ∀ (i : I), Dvd.dvd (s i) z) : Dvd.dvd (Finset.univ.prod 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) : Iff (Exists fun (μ : I → R) => Eq (t.sum fun (i : I) => HMul.hMul (μ i) ((SDiff.sdiff t (Singleton.singleton i)).prod fun (j : I) => s j)) 1) (Pairwise (Function.onFun IsCoprime fun (i : Subtype fun (x : I) => Membership.mem t x) => s i.val))

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] : Iff (Exists fun (μ : I → R) => Eq (Finset.univ.sum fun (i : I) => HMul.hMul (μ i) ((HasCompl.compl (Singleton.singleton i)).prod fun (j : I) => s j)) 1) (Pairwise (Function.onFun IsCoprime s))

theorem pairwise_coprime_iff_coprime_prod {R : Type u} {I : Type v} [CommSemiring R] {s : I → R} {t : Finset I} [DecidableEq I] : Iff (Pairwise (Function.onFun IsCoprime fun (i : Subtype fun (x : I) => Membership.mem t x) => s i.val)) (∀ (i : I), Membership.mem t i → IsCoprime (s i) ((SDiff.sdiff t (Singleton.singleton i)).prod fun (j : I) => s j))

theorem IsCoprime.pow_left {R : Type u} [CommSemiring R] {x y : R} {m : Nat} (H : IsCoprime x y) : IsCoprime (HPow.hPow x m) y

theorem IsCoprime.pow_right {R : Type u} [CommSemiring R] {x y : R} {n : Nat} (H : IsCoprime x y) : IsCoprime x (HPow.hPow y n)

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

theorem IsCoprime.pow_left_iff {R : Type u} [CommSemiring R] {x y : R} {m : Nat} (hm : LT.lt 0 m) : Iff (IsCoprime (HPow.hPow x m) y) (IsCoprime x y)

theorem IsCoprime.pow_right_iff {R : Type u} [CommSemiring R] {x y : R} {m : Nat} (hm : LT.lt 0 m) : Iff (IsCoprime x (HPow.hPow y m)) (IsCoprime x y)

theorem IsCoprime.pow_iff {R : Type u} [CommSemiring R] {x y : R} {m n : Nat} (hm : LT.lt 0 m) (hn : LT.lt 0 n) : Iff (IsCoprime (HPow.hPow x m) (HPow.hPow y n)) (IsCoprime x y)

theorem IsRelPrime.prod_left {α : Type u_2} {I : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x : α} {s : I → α} {t : Finset I} : (∀ (i : I), Membership.mem t i → IsRelPrime (s i) x) → IsRelPrime (t.prod 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 : I), Membership.mem t i → IsRelPrime x (s i)) → IsRelPrime x (t.prod 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} : Iff (IsRelPrime (t.prod fun (i : I) => s i) x) (∀ (i : I), Membership.mem t i → IsRelPrime (s i) x)

theorem IsRelPrime.prod_right_iff {α : Type u_1} {I : Type u_2} [CommMonoid α] [DecompositionMonoid α] {x : α} {s : I → α} {t : Finset I} : Iff (IsRelPrime x (t.prod fun (i : I) => s i)) (∀ (i : I), Membership.mem t i → 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 (t.prod fun (i : I) => s i) x) (i : I) (hit : Membership.mem t i) : 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 (t.prod fun (i : I) => s i)) (i : I) (hit : Membership.mem t i) : 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.toSet.Pairwise (Function.onFun IsRelPrime s) → (∀ (i : I), Membership.mem t i → Dvd.dvd (s i) z) → Dvd.dvd (t.prod 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 (Function.onFun IsRelPrime s)) (Hs1 : ∀ (i : I), Dvd.dvd (s i) z) : Dvd.dvd (Finset.univ.prod 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] : Iff (Pairwise (Function.onFun IsRelPrime fun (i : Subtype fun (x : I) => Membership.mem t x) => s i.val)) (∀ (i : I), Membership.mem t i → IsRelPrime (s i) ((SDiff.sdiff t (Singleton.singleton i)).prod fun (j : I) => s j))

theorem IsRelPrime.pow_left {α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x y : α} {m : Nat} (H : IsRelPrime x y) : IsRelPrime (HPow.hPow x m) y

theorem IsRelPrime.pow_right {α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x y : α} {n : Nat} (H : IsRelPrime x y) : IsRelPrime x (HPow.hPow y n)

theorem IsRelPrime.pow {α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x y : α} {m n : Nat} (H : IsRelPrime x y) : IsRelPrime (HPow.hPow x m) (HPow.hPow y n)

theorem IsRelPrime.pow_left_iff {α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x y : α} {m : Nat} (hm : LT.lt 0 m) : Iff (IsRelPrime (HPow.hPow x m) y) (IsRelPrime x y)

theorem IsRelPrime.pow_right_iff {α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x y : α} {m : Nat} (hm : LT.lt 0 m) : Iff (IsRelPrime x (HPow.hPow y m)) (IsRelPrime x y)

theorem IsRelPrime.pow_iff {α : Type u_1} [CommMonoid α] [DecompositionMonoid α] {x y : α} {m n : Nat} (hm : LT.lt 0 m) (hn : LT.lt 0 n) : Iff (IsRelPrime (HPow.hPow x m) (HPow.hPow y n)) (IsRelPrime x y)