self_zpow₀

Mathlib.Algebra.GroupWithZero.Semiconj

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

English

The same as zpow_self₀: a commutes with its powers.

Русский

То же самое, что и zpow_self₀: a коммути́рует с своими степенями.

LaTeX

$$$\forall n \in \mathbb{Z},\ Commute a (a^{n})$$$

Lean4

theorem self_zpow₀ (a : G₀) (n : ℤ) : Commute a (a ^ n) :=
  (Commute.refl a).zpow_right₀ n

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

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

Разделы

Аффилиация

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