Products over a set of prime factors

A product of distinct primes taken from n.primeFactors is squarefree, divides n, and introduces no prime that n does not already have; and it is coprime to any prime left out of the set. These are the facts an induction over the primes of n spends at each step, when it peels one prime off and recurses on the rest.

Main results

• TauCeti.squarefree_prod_and_coprime_of_subset_primeFactors: the three facts above, for a subset of n.primeFactors and a prime outside it.

theorem TauCeti.squarefree_prod_and_coprime_of_subset_primeFactors {n : ℕ} [NeZero n] {S : Finset ℕ} (hS : S ⊆ n.primeFactors) {p : ℕ} (hp : Nat.Prime p) (hpS : p ∉ S) : Squarefree (S.prod id) ∧ p.Coprime (S.prod id) ∧ (S.prod id).primeFactors ⊆ n.primeFactors

A product of some of n's prime factors is squarefree, coprime to any prime left out, and introduces no new prime. For S ⊆ n.primeFactors and a prime p ∉ S, the product ∏ q ∈ S, q is squarefree (the members are distinct primes), coprime to p (it is coprime to each member), and its prime factors are again among n's (it divides n).