npow_mul_comm

Mathlib.Algebra.Group.NatPowAssoc

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

English

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

Русский

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

LaTeX

$$$ x^m x^n = x^n x^m $$$

Lean4

theorem npow_mul_comm (m n : ℕ) (x : M) : x ^ m * x ^ n = x ^ n * x ^ m := by simp only [← npow_add, add_comm]

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

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

Разделы

Аффилиация

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