integral_div — Mathlib

English

For f: ℝ → ℝ, the interval integral equals the real integral embedded in the complex plane via ofReal.

Русский

Для f: ℝ → ℝ интеграл по интервалу совпадает с вещественным интегралом, приводимым в комплексную плоскость через ofReal.

LaTeX

$$$\int_{a}^{b} (f(x) : ℂ) \, dμ = \mathbb{C}.ofReal (\int_{a}^{b} f(x) \, dμ)$$$

Lean4

@[simp]
theorem integral_div {𝕜 : Type*} [RCLike 𝕜] (r : 𝕜) (f : ℝ → 𝕜) : ∫ x in a..b, f x / r ∂μ = (∫ x in a..b, f x ∂μ) / r :=
  by simpa only [div_eq_mul_inv] using integral_mul_const r⁻¹ f

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