ppow_mul_comm

Mathlib.Algebra.Group.PNatPowAssoc

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

English

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

Русский

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

LaTeX

$$$x^{m} \\cdot x^{n} = x^{n} \\cdot x^{m}$$$

Lean4

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

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

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

Разделы

Аффилиация

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