exp_smul — Mathlib

English

Let G act on 𝔸 by a continuous semiring action; then exp(g • x) = g • exp(x).

Русский

Пусть моноид G действует на 𝔸 непрерывно через скалярное действие; тогда exp(g • x) = g • exp(x).

LaTeX

$$$\\exp 𝕂(g \\cdot x) = g \\cdot \\exp 𝕂 x$$$

Lean4

theorem exp_smul {G} [Monoid G] [MulSemiringAction G 𝔸] [ContinuousConstSMul G 𝔸] (g : G) (x : 𝔸) :
    exp 𝕂 (g • x) = g • exp 𝕂 x :=
  (map_exp 𝕂 (MulSemiringAction.toRingHom G 𝔸 g) (continuous_const_smul g) x).symm

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