Products over a finite set of primes

In a unique factorization monoid whose only unit is 1, the passage from a finite set S of primes to the product ∏ p ∈ S, p loses no information: the normalized factors of the product are exactly the elements of S, distinct sets of primes have distinct products, and every divisor of the product is the product of a subset of S.

These are the facts that turn a divisibility statement about a product of distinct primes into a statement about subsets of the set of factors. The hypothesis on the units is what makes the conclusions equalities rather than statements up to associates; the motivating example is the multiplicative monoid of ideals of a Dedekind domain.

@[simp]

theorem TauCeti.normalizedFactors_finset_prod_of_prime {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] [StrongNormalizationMonoid α] [Subsingleton αˣ] {S : Finset α} (hS : ∀ p ∈ S, Prime p) : UniqueFactorizationMonoid.normalizedFactors (∏ p ∈ S, p) = S.val

The normalized factors of the product of a finite set of primes are that set.

@[simp]

theorem TauCeti.finset_prod_eq_iff_of_prime {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] [StrongNormalizationMonoid α] [Subsingleton αˣ] {S T : Finset α} (hS : ∀ p ∈ S, Prime p) (hT : ∀ p ∈ T, Prime p) : ∏ p ∈ S, p = ∏ p ∈ T, p ↔ S = T

A finite set of primes is determined by its product.

theorem TauCeti.exists_subset_finset_prod_eq_of_dvd {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] [StrongNormalizationMonoid α] [Subsingleton αˣ] {S : Finset α} [Nontrivial α] (hS : ∀ p ∈ S, Prime p) {a : α} (hdvd : a ∣ ∏ p ∈ S, p) : ∃ T ⊆ S, a = ∏ p ∈ T, p

Every divisor of a product of distinct primes is the product of a subset of them.