exp_apply — Mathlib

English

For nilpotent D, the underlying linear map of exp(D) acts in the same way as the exponential of the underlying linear map; i.e., the map D.exp h, applied to l, equals IsNilpotent.exp(D.toLinearMap)(l).

Русский

Для нильпотентной деривации D, отображение exp(D) действует так же, как экспонента от базового линейного отображения.

LaTeX

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

Lean4

theorem exp_apply (h : IsNilpotent D.toLinearMap) : exp D h = IsNilpotent.exp D.toLinearMap :=
  rfl

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