curveIntegral_restrictScalars — Mathlib

English

The curve integral is invariant under restriction of scalars: integrating (ω x).restrictScalars 𝕝 over γ equals integrating ω x over γ.

Русский

Криволинейный интеграл сохраняется при ограничении скалярами: интеграл (ω x).restrictScalars 𝕝 по γ равен интегралу ω x по γ.

LaTeX

$$$\\int_{\\gamma} (\\omega x).restrictScalars 𝕝 = \\int_{\\gamma} \\omega x$$$

Lean4

@[simp]
theorem curveIntegral_restrictScalars : ∫ᶜ x in γ, (ω x).restrictScalars 𝕝 = ∫ᶜ x in γ, ω x :=
  by
  letI : NormedSpace ℝ F := .restrictScalars ℝ 𝕜 F
  simp [curveIntegral_def]

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