Shared rational and polynomial valuation bounds

The local API reuses the existing Zeta5Irrational valuation and integral-polynomial toolkit. Only the product identity and the inverse bound without a nonzero premise are specific here.

theorem Zeta32.Arith.Local.padicValRat_finset_prod {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} (s : Finset ι) (f : ι → ℚ) (hf : ∀ i ∈ s, f i ≠ 0) : padicValRat p (∏ i ∈ s, f i) = ∑ i ∈ s, padicValRat p (f i)

Valuation is additive on a finite product of nonzero rational factors.

theorem Zeta32.Arith.Local.VG.inv {p : ℕ} [Fact (Nat.Prime p)] {q r : ℚ} (hv : ↑(padicValRat p q) ≤ r) : VG p q⁻¹ (-r)