zpow_right — Mathlib

English

If a and b commute, then a commutes with every power of b, i.e., a and b^{m} commute for all integers m.

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem zpow_right (h : Commute a b) (m : ℤ) : Commute a (b ^ m) :=
  SemiconjBy.zpow_right h m

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