hasFDerivAt_intCast

Mathlib.Analysis.Calculus.FDeriv.Const

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

English

Let z ∈ ℤ and x ∈ E. The derivative at x of the int cast z is the zero linear map.

Русский

Пусть z ∈ ℤ и x ∈ E. Производная в точке x отображения z, приводимого в F, равна нулю.

LaTeX

$$$HasFDerivAt (z : E \to F) (0 : E \toL[𝕜] F) x$$$

Lean4

@[fun_prop]
theorem hasFDerivAt_intCast [IntCast F] (z : ℤ) (x : E) : HasFDerivAt (z : E → F) (0 : E →L[𝕜] F) x :=
  hasFDerivAt_const _ _

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

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

Разделы

Аффилиация

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