Theorem: RectangleIntegral.const_smul (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, HIntegral, VIntegral, smul_add, smul_sub, smul_smul, mul_comm]
State after:
no goals