exp_smul — Mathlib

English

If G acts on A by semiring action and a ∈ A is nilpotent, then exp(g • a) = g • exp(a) for every g ∈ G.

Русский

Если элемент nиль-потентен в пространстве A и действует скаляром через $G$, то экспонента удовлетворяет $\exp(g\cdot a) = g\cdot\exp(a)$ для всякого $g \in G$.

LaTeX

$$$\exp(g \cdot a) = g \cdot \exp(a)$$$

Lean4

theorem exp_smul {G : Type*} [Monoid G] [MulSemiringAction G A] (g : G) {a : A} (ha : IsNilpotent a) :
    exp (g • a) = g • exp a :=
  (map_exp ha (MulSemiringAction.toRingHom G A g)).symm

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