self_zpow

Mathlib.Algebra.Group.Commute.Basic

URI: https://scilib.ai/kg/mathlib#Commute.self_zpow

English

An element a commutes with its own powers: a and a^{n} commute for any integer n.

Русский

Элемент a коммутирует со своими степенями: a и a^{n} коммутируют для любого целого n.

LaTeX

$$$ \\text{Commute } a (a^{n}) $$$

Lean4

@[to_additive]
theorem self_zpow : Commute a (a ^ n) :=
  (Commute.refl a).zpow_right n

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

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

Разделы

Аффилиация

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