torusIntegral_const_mul — Mathlib

English

For a scalar a ∈ ℂ, torusIntegral(a · f) = a · torusIntegral(f).

Русский

Для константного скаляра a ∈ ℂ: torusIntegral(a · f) = a · torusIntegral(f).

LaTeX

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

Lean4

theorem torusIntegral_const_mul (a : ℂ) (f : (ℂⁿ) → ℂ) (c : ℂⁿ) (R : ℝⁿ) :
    (∯ x in T(c, R), a * f x) = a * ∯ x in T(c, R), f x :=
  torusIntegral_smul a f c R

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