zpow_right₀

Mathlib.Algebra.GroupWithZero.Semiconj

URI: https://scilib.ai/kg/mathlib#Commute.zpow_right₀

English

If a and b commute, then a^m and b^n commute for any integers m,n.

Русский

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

LaTeX

$$For all m,n ∈ ℤ, Commute a^m (b^n)$$

Lean4

theorem zpow_right₀ (h : Commute a b) : ∀ m : ℤ, Commute a (b ^ m) :=
  SemiconjBy.zpow_right₀ h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru