S-factored numbers and p-adic valuations

Mathlib's Nat.factoredNumbers S is the set of positive integers all of whose prime factors lie in the finite set S. This file describes these numbers through p-adic valuations:

• TauCeti.forall_padicValRat_eq_zero_iff_mem_factoredNumbers: a nonzero rational number has p-adic valuation zero at every prime p ∉ S exactly when its numerator (in absolute value) and its denominator are S-factored;
• TauCeti.prod_pow_padicValNat_eq_self_of_mem_factoredNumbers: if S consists of primes, an S-factored number is the product of the powers p ^ v_p(n) over p ∈ S.

These are the arithmetic inputs for describing the rational S-units.

theorem TauCeti.forall_padicValRat_eq_zero_iff_mem_factoredNumbers {S : Finset ℕ} {q : ℚ} (hq : q ≠ 0) : (∀ (p : ℕ), Nat.Prime p → p ∉ S → padicValRat p q = 0) ↔ q.num.natAbs ∈ Nat.factoredNumbers S ∧ q.den ∈ Nat.factoredNumbers S

A nonzero rational number has p-adic valuation zero at every prime p ∉ S exactly when the absolute value of its numerator and its denominator are S-factored.

theorem TauCeti.prod_pow_padicValNat_eq_self_of_mem_factoredNumbers {S : Finset ℕ} (hS : ∀ p ∈ S, Nat.Prime p) {n : ℕ} (hn : n ∈ Nat.factoredNumbers S) : ∏ p ∈ S, p ^ padicValNat p n = n

If S consists of primes, an S-factored number n is the product of the prime powers p ^ v_p(n) over p ∈ S.