Theorem: RectangleIntegral.const_mul' (PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g : ℂ → E
z✝ w✝ p c✝ A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f : ℂ → E
z w c : ℂ
⊢ RectangleIntegral' (fun s => c • f s) z w = c • RectangleIntegral' f z w
Tactic:
simp [RectangleIntegral', RectangleIntegral.const_smul, smul_smul]
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g : ℂ → E
z✝ w✝ p c✝ A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f : ℂ → E
z w c : ℂ
⊢ (I * ((↑π)⁻¹ * 2⁻¹) * c) • RectangleIntegral (fun s => f s) z w = (c * (I * ((↑π)⁻¹ * 2⁻¹))) • RectangleIntegral f z w

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f✝ g : ℂ → E
z✝ w✝ p c✝ A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
f : ℂ → E
z w c : ℂ
⊢ (I * ((↑π)⁻¹ * 2⁻¹) * c) • RectangleIntegral (fun s => f s) z w = (c * (I * ((↑π)⁻¹ * 2⁻¹))) • RectangleIntegral f z w
Tactic:
ring_nf
State after:
no goals