ppow_mul_assoc

Mathlib.Algebra.Group.PNatPowAssoc

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

English

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

Русский

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

LaTeX

$$$(x^k \\cdot x^m) \\cdot x^n = x^k \\cdot (x^m \\cdot x^n)$$$

Lean4

theorem ppow_mul_assoc (k m n : ℕ+) (x : M) : (x ^ k * x ^ m) * x ^ n = x ^ k * (x ^ m * x ^ n) := by
  simp only [← ppow_add, add_assoc]

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

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

Разделы

Аффилиация

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