mathlib documentation

ring_theory.coprime.lemmas

Additional lemmas about elements of a ring satisfying is_coprime #

These lemmas are in a separate file to the definition of is_coprime as they require more imports.

Notably, this includes lemmas about finset.prod as this requires importing big_operators, and lemmas about has_pow since these are easiest to prove via finset.prod.

theorem is_coprime.prod_left {R : Type u} {I : Type v} [comm_semiring R] {x : R} {s : I → R} {t : finset I} :
(∀ (i : I), i tis_coprime (s i) x)is_coprime (∏ (i : I) in t, s i) x
theorem is_coprime.prod_right {R : Type u} {I : Type v} [comm_semiring R] {x : R} {s : I → R} {t : finset I} :
(∀ (i : I), i tis_coprime x (s i))is_coprime x (∏ (i : I) in t, s i)
theorem is_coprime.prod_left_iff {R : Type u} {I : Type v} [comm_semiring R] {x : R} {s : I → R} {t : finset I} :
is_coprime (∏ (i : I) in t, s i) x ∀ (i : I), i tis_coprime (s i) x
theorem is_coprime.prod_right_iff {R : Type u} {I : Type v} [comm_semiring R] {x : R} {s : I → R} {t : finset I} :
is_coprime x (∏ (i : I) in t, s i) ∀ (i : I), i tis_coprime x (s i)
theorem is_coprime.of_prod_left {R : Type u} {I : Type v} [comm_semiring R] {x : R} {s : I → R} {t : finset I} (H1 : is_coprime (∏ (i : I) in t, s i) x) (i : I) (hit : i t) :
is_coprime (s i) x
theorem is_coprime.of_prod_right {R : Type u} {I : Type v} [comm_semiring R] {x : R} {s : I → R} {t : finset I} (H1 : is_coprime x (∏ (i : I) in t, s i)) (i : I) (hit : i t) :
is_coprime x (s i)
theorem finset.prod_dvd_of_coprime {R : Type u} {I : Type v} [comm_semiring R] {z : R} {s : I → R} {t : finset I} (Hs : t.pairwise (is_coprime on s)) (Hs1 : ∀ (i : I), i ts i z) :
∏ (x : I) in t, s x z
theorem fintype.prod_dvd_of_coprime {R : Type u} {I : Type v} [comm_semiring R] {z : R} {s : I → R} [fintype I] (Hs : pairwise (is_coprime on s)) (Hs1 : ∀ (i : I), s i z) :
∏ (x : I), s x z
theorem is_coprime.pow_left {R : Type u} [comm_semiring R] {x y : R} {m : } (H : is_coprime x y) :
is_coprime (x ^ m) y
theorem is_coprime.pow_right {R : Type u} [comm_semiring R] {x y : R} {n : } (H : is_coprime x y) :
is_coprime x (y ^ n)
theorem is_coprime.pow {R : Type u} [comm_semiring R] {x y : R} {m n : } (H : is_coprime x y) :
is_coprime (x ^ m) (y ^ n)
theorem is_coprime.pow_left_iff {R : Type u} [comm_semiring R] {x y : R} {m : } (hm : 0 < m) :
theorem is_coprime.pow_right_iff {R : Type u} [comm_semiring R] {x y : R} {m : } (hm : 0 < m) :
theorem is_coprime.pow_iff {R : Type u} [comm_semiring R] {x y : R} {m n : } (hm : 0 < m) (hn : 0 < n) :
is_coprime (x ^ m) (y ^ n) is_coprime x y