Theorems · Theorem · commutative algebra

Finset.prod_dvd_of_isRelPrime

∀ {α : Type u_2} {I : Type u_1} [inst : CommMonoid α] [DecompositionMonoid α] {z : α} {s : I → α} {t : Finset I},
  (↑t).Pairwise (Function.onFun IsRelPrime s) → (∀ i ∈ t, s i ∣ z) → ∏ x ∈ t, s x ∣ z

Defined in

Mathlib.RingTheory.Coprime.Lemmas

Cited by

3 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidDecompositionMonoid