zpow_zpow_self₀ — Mathlib

English

Let G be a group with zero and a ∈ G. Then for all integers m,n, the elements a^m and a^n commute.

Русский

Пусть G — группа с нулём, и a ∈ G. Тогда для любых целых m,n элементы a^m и a^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

theorem zpow_zpow_self₀ (a : G₀) (m n : ℤ) : Commute (a ^ m) (a ^ n) :=
  (Commute.refl a).zpow_zpow₀ m n

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