exp_zsmul

Mathlib.Algebra.GroupWithZero.WithZero

URI: https://scilib.ai/kg/mathlib#WithZero.exp_zsmul

English

For any integer n and a in G, exp(n • a) equals (exp a) raised to the n-th power.

Русский

Для любой целой степени n и элемента a∈G выполняется exp(n • a) = (exp a)^{n}.

LaTeX

$$$\exp(n \cdot a) = (\exp a)^{n} \quad (n \in \mathbb{Z},\ a \in G)$$$

Lean4

@[simp← ]
theorem exp_zsmul (n : ℤ) (a : G) : exp (n • a) = exp a ^ n :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru