integral_div — Mathlib

English

Division by a nonzero scalar is valid under the integral: ∫ f / r = (∫ f) / r.

Русский

Деление на ненулевой скаляр сохраняется под интегралом: ∫ f / r = (∫ f) / r.

LaTeX

$$$\int a, f(a) / r \partial\mu = (\int a, f(a) \partial\mu) / r$$$

Lean4

theorem integral_div {L : Type*} [RCLike L] (r : L) (f : α → L) : ∫ a, f a / r ∂μ = (∫ a, f a ∂μ) / r := by
  simpa only [← div_eq_mul_inv] using integral_mul_const r⁻¹ f

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