zpow_left — Mathlib

English

If A and B commute, then A^{m} and B^{n} commute for all integers m,n. More precisely, Commute(A^{m}, B^{n}) when Commute(A,B).

Русский

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

LaTeX

$$$$\\text{If }\\ commute(A,B), \\text{ then } A^{m} \\;\\text{commutes with } B^{n} \\text{ for all } m,n\\in\\mathbb{Z}.$$$

Lean4

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

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