Theorems · Theorem · commutative algebra

UniqueFactorizationMonoid.prime_pow_coprime_prod_of_coprime_insert

∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α] [inst_2 : DecidableEq α] {s : Finset α}
  (i : α → ℕ),
  ∀ p ∉ s,
    (∀ q ∈ insert p s, Prime q) →
      (∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q') → IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')

Defined in

Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroUniqueFactorizationMonoidDecidableEq