zpow_zpow — Mathlib

English

If A and B commute, then A^{m} and B^{n} commute for all integers m,n. (This is the universal commuting property for z-powers.)

Русский

Если A и B коммутируют, то A^{m} и B^{n} коммутируют для любых целых m,n.

LaTeX

$$$$\\text{Commute}(A^{m}, B^{n}) \\text{ for all } m,n \\in \\mathbb{Z}.$$$$

Lean4

theorem zpow_zpow {A B : M} (h : Commute A B) (m n : ℤ) : Commute (A ^ m) (B ^ n) :=
  Commute.zpow_right (Commute.zpow_left h _) _

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