units_zpow_left — Mathlib

English

If a commutes with the underlying value of a unit u, then u^m commutes with a for all integers m.

Русский

Если единица u в некоторых условиях коммутирует с a, то u^m коммутирует с a для любого целого m.

LaTeX

$$Commute (↑u) a \Rightarrow Commute (↑(u^m)) a$$

Lean4

@[to_additive (attr := simp)]
theorem units_zpow_left (h : Commute (↑u) a) (m : ℤ) : Commute (↑(u ^ m)) a :=
  (h.symm.units_zpow_right m).symm

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