zpow_zpow — Mathlib

English

If a and b commute, then their powers commute with each other: a^{m} and b^{n} commute for all integers m,n.

Русский

Если a и b коммутируют, то их степени коммутируют друг с другом: a^{m} и b^{n} коммутируют для всех целых m,n.

LaTeX

$$$ \\text{Commute } a b \\Rightarrow \\forall m,n \\in \\mathbb{Z},\\ \\text{Commute } (a^{m}) (b^{n}) $$$

Lean4

@[to_additive]
theorem zpow_zpow (h : Commute a b) (m n : ℤ) : Commute (a ^ m) (b ^ n) :=
  (h.zpow_left m).zpow_right n

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