npow_mul_assoc

Mathlib.Algebra.Group.NatPowAssoc

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

English

For all k,m,n ∈ ℕ and x ∈ M, (x^k * x^m) * x^n = x^k * (x^m * x^n).

Русский

Для любых k,m,n ∈ ℕ и x ∈ M выполняется (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 npow_mul_assoc (k m n : ℕ) (x : M) : (x ^ k * x ^ m) * x ^ n = x ^ k * (x ^ m * x ^ n) := by
  simp only [← npow_add, add_assoc]

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

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

Разделы

Аффилиация

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