integral_smul_const — Mathlib

English

If a ∈ ℂ and f: ℂ → ℂ, then circleIntegral of a · f equals a times the circleIntegral of f.

Русский

Если a ∈ ℂ и f: ℂ → ℂ, то круговой интеграл a·f равен a·круговому интегралу f.

LaTeX

$$$\\oint z in C(c,R), a \\cdot f(z) = a \\cdot (\\oint z in C(c,R), f(z))$$$

Lean4

@[simp]
theorem integral_smul_const [CompleteSpace E] (f : ℂ → ℂ) (a : E) (c : ℂ) (R : ℝ) :
    (∮ z in C(c, R), f z • a) = (∮ z in C(c, R), f z) • a := by
  simp only [circleIntegral, intervalIntegral.integral_smul_const, ← smul_assoc]

Похожие утверждения