exp_map_apply — Mathlib

English

The pointwise action of exp(D) on an element l equals the corresponding exponential map applied to l.

Русский

Пусть l — элемент L; тогда exp(D) применимо к l так же, как экспонента применяется к l.

LaTeX

$$D.exp h l = IsNilpotent.exp D.toLinearMap l$$

Lean4

theorem exp_map_apply (h : IsNilpotent D.toLinearMap) (l : L) : exp D h l = IsNilpotent.exp D.toLinearMap l :=
  DFunLike.congr_fun (exp_apply D h) l

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