npow_mul'

Mathlib.Algebra.Group.NatPowAssoc

URI: https://scilib.ai/kg/mathlib#npow_mul'

English

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

Русский

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

LaTeX

$$$ x^{mn} = (x^n)^m $$$

Lean4

theorem npow_mul' (x : M) (m n : ℕ) : x ^ (m * n) = (x ^ n) ^ m :=
  by
  rw [mul_comm]
  exact npow_mul x n m

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

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

Разделы

Аффилиация

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