zpow_mul_comm

Mathlib.Algebra.Group.Basic

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

English

For any a ∈ G and integers m,n, a^m and a^n commute: a^m a^n = a^n a^m.

Русский

Для любого a ∈ G и целых m,n степени коммутируют: a^m a^n = a^n a^m.

LaTeX

$$$\forall a \in G,\ \forall m,n \in \mathbb{Z},\ a^{m} a^{n} = a^{n} a^{m}$$$

Lean4

@[to_additive]
theorem zpow_mul_comm (a : G) (m n : ℤ) : a ^ m * a ^ n = a ^ n * a ^ m := by rw [← zpow_add, Int.add_comm, zpow_add]

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

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

Разделы

Аффилиация

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