extendTo𝕜_apply

Mathlib.Analysis.RCLike.Extend

URI: https://scilib.ai/kg/mathlib#LinearMap.extendTo𝕜_apply

English

For fr : Dual Real F, the value at x is fr(x) − i fr(i x).

Русский

Для fr : Dual Real F значение в x равно fr(x) − i fr(i x).

LaTeX

$$$ (fr.extendTo𝕜')(x) = (fr(x) : 𝕜) - i (fr(i x) : 𝕜) $$$

Lean4

theorem extendTo𝕜_apply (fr : RestrictScalars ℝ 𝕜 F →ₗ[ℝ] ℝ) (x : F) :
    fr.extendTo𝕜 x = (fr x : 𝕜) - (I : 𝕜) * (fr ((I : 𝕜) • x) : 𝕜) :=
  rfl

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

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

Разделы

Аффилиация

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