torusIntegral_smul — Mathlib

English

For a scalar a from a field 𝕜, torusIntegral(a · f) = a · torusIntegral(f).

Русский

Для скаляра a из поля 𝕜: torusIntegral(a · f) = a · torusIntegral(f).

LaTeX

$$$\operatorname{torusIntegral}(a \cdot f,c,R) = a \cdot \operatorname{torusIntegral}(f,c,R)$$$

Lean4

theorem torusIntegral_smul {𝕜 : Type*} [RCLike 𝕜] [NormedSpace 𝕜 E] [SMulCommClass 𝕜 ℂ E] (a : 𝕜) (f : (ℂⁿ) → E)
    (c : ℂⁿ) (R : ℝⁿ) : (∯ x in T(c, R), a • f x) = a • ∯ x in T(c, R), f x := by
  simp only [torusIntegral, integral_smul, ← smul_comm a (_ : ℂ) (_ : E)]

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