integral_smul — Mathlib

English

For a scalar a in 𝕜, and f: ℂ → E circle-integral of a • f equals a times the circle-integral of f.

Русский

Для скаляра a в 𝕜 и функции f: ℂ → E круговой интеграл a • f(z) равен 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 {𝕜 : Type*} [RCLike 𝕜] [NormedSpace 𝕜 E] [SMulCommClass 𝕜 ℂ E] (a : 𝕜) (f : ℂ → E) (c : ℂ)
    (R : ℝ) : (∮ z in C(c, R), a • f z) = a • ∮ z in C(c, R), f z := by
  simp only [circleIntegral, ← smul_comm a (_ : ℂ) (_ : E), intervalIntegral.integral_smul]

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