ppow_add

Mathlib.Algebra.Group.PNatPowAssoc

URI: https://scilib.ai/kg/mathlib#ppow_add

English

For x ∈ M and k, n ∈ ℕ+, x^(k+n) = x^k · x^n.

Русский

Для x ∈ M и k, n ∈ ℕ+, выполняется x^(k+n) = x^k · x^n.

LaTeX

$$$x^{(k+n)} = x^{k} \\cdot x^{n}$$$

Lean4

theorem ppow_add (k n : ℕ+) (x : M) : x ^ (k + n) = x ^ k * x ^ n :=
  PNatPowAssoc.ppow_add k n x

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

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

Разделы

Аффилиация

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