simp only [f, map_div₀, map_mul, map_add, map_one]
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ f x ((starRingEnd ℂ) s) = (starRingEnd ℂ) (f x s)
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ ↑x ^ (starRingEnd ℂ) s / ((starRingEnd ℂ) s * ((starRingEnd ℂ) s + 1)) =
    (starRingEnd ℂ) (↑x ^ s) / ((starRingEnd ℂ) s * ((starRingEnd ℂ) s + 1))