extDeriv_fun_smul

Mathlib.Analysis.Calculus.DifferentialForm.Basic

URI: https://scilib.ai/kg/mathlib#extDeriv_fun_smul

English

For a scalar c in 𝕜 and a ω, the extDeriv of (c • ω) equals c • extDeriv ω.

Русский

Для скаляра c и формы ω, extDeriv (c • ω) = c • extDeriv ω.

LaTeX

$$$\text{extDeriv}(c \cdot \omega) = c \cdot \text{extDeriv}(\omega).$$$

Lean4

theorem extDeriv_fun_smul (c : 𝕜) (ω : E → E [⋀^Fin n]→L[𝕜] F) : extDeriv (c • ω) x = c • extDeriv ω x :=
  extDeriv_smul c ω

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru