rw [prod_const, card_fin]
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∏ _i : Fin k, ∑ d ∈ P.divisors, if ↑d ≤ x then (↑d)⁻¹ else 0) = (∑ d ∈ P.divisors, if ↑d ≤ x then (↑d)⁻¹ else 0) ^ k
no goals