Theorem: Perron.keyIdentity (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
x✝ σ σ' σ'' T x : ℝ
s : ℂ
s_ne_zero : s ≠ 0
s_ne_neg_one : s ≠ -1
⊢ ↑x ^ s / (s * (s + 1)) = ↑x ^ s / s - ↑x ^ s / (s + 1)
Tactic:
field_simp [sPlusOneNeZero, mul_ne_zero]
State after:
x✝ σ σ' σ'' T x : ℝ
s : ℂ
s_ne_zero : s ≠ 0
s_ne_neg_one : s ≠ -1
⊢ ↑x ^ s = ↑x ^ s * (s + 1) - s * ↑x ^ s

State before:
x✝ σ σ' σ'' T x : ℝ
s : ℂ
s_ne_zero : s ≠ 0
s_ne_neg_one : s ≠ -1
⊢ ↑x ^ s = ↑x ^ s * (s + 1) - s * ↑x ^ s
Tactic:
ring_nf
State after:
no goals