theorem base_dvd_prod_exp {ι : Type u_1} [DecidableEq ι] {S : Finset ι} {sp : ι} {f_base f_exp : ι → ℕ} (sp_in_S : sp ∈ S) (h_exp_pos : 0 < f_exp sp) : f_base sp ∣ ∏ s ∈ S, f_base s ^ f_exp s

theorem z_prod_prime_pow_eq_one_iff {ι : Type u_1} [DecidableEq ι] {S : Finset ι} (f_prime : ι → ℕ) (f_exp : ι → ℤ) (h_primes : ∀ s ∈ S, Nat.Prime (f_prime s)) (h_f_prime_inj : Function.Injective f_prime) : ∏ s ∈ S, ↑(f_prime s) ^ f_exp s = 1 ↔ ∀ p ∈ S, f_exp p = 0

theorem q_prod_prime_pow_eq_one_iff {ι : Type u_1} [DecidableEq ι] {S : Finset ι} {f_prime : ι → ℕ} (f_exp : ι → ℚ) (h_primes : ∀ s ∈ S, Nat.Prime (f_prime s)) (h_f_prime_inj : Function.Injective f_prime) : ∏ s ∈ S, ↑(f_prime s) ^ ↑(f_exp s) = 1 ↔ ∀ p ∈ S, f_exp p = 0