zpow_comm

Mathlib.Algebra.Group.Basic

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

English

For any a ∈ α and integers m,n, (a^m)^n = (a^n)^m.

Русский

Для любого a ∈ α и целых m,n, (a^m)^n = (a^n)^m.

LaTeX

$$$(a^{m})^{n} = (a^{n})^{m}$$$

Lean4

@[to_additive]
theorem zpow_comm (a : α) (m n : ℤ) : (a ^ m) ^ n = (a ^ n) ^ m := by rw [← zpow_mul, zpow_mul']

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

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

Разделы

Аффилиация

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