hasFDerivAt_exp_zero — Mathlib

English

The Fréchet derivative of exp at zero is the identity map.

Русский

Производная Фреше экспоненты в нуле равна тождественному отображению.

LaTeX

$$$$ \HasFDerivAt(\exp, 1, 0) $$$$

Lean4

/-- The exponential in a Banach algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ` has Fréchet derivative
`1 : 𝔸 →L[𝕂] 𝔸` at zero. -/
theorem hasFDerivAt_exp_zero : HasFDerivAt (exp 𝕂) (1 : 𝔸 →L[𝕂] 𝔸) 0 :=
  hasStrictFDerivAt_exp_zero.hasFDerivAt

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