exp_nsmul

Mathlib.Algebra.GroupWithZero.WithZero

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

English

For n ∈ ℕ and a ∈ M, exp (n • a) = (exp a) ^ n.

Русский

Для n ∈ ℕ и a ∈ M: exp (n • a) = (exp a)^n.

LaTeX

$$$\\exp(n \\cdot a) = (\\exp a)^{n}$$$

Lean4

@[simp← ]
theorem exp_nsmul (n : ℕ) (a : M) : exp (n • a) = exp a ^ n :=
  rfl

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

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

Разделы

Аффилиация

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