extendDomain_zpow

Mathlib.Algebra.Group.End

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.extendDomain_zpow

English

For integer powers n, (e^n).extendDomain f = e.extendDomain f^n.

Русский

Для целочисленных степеней n: (e^n).extendDomain f = e.extendDomain f^n.

LaTeX

$$$(e^{n}).extendDomain f = e.extendDomain f^{n}$$$

Lean4

@[simp]
theorem extendDomain_zpow (n : ℤ) : (e ^ n).extendDomain f = e.extendDomain f ^ n :=
  map_zpow (extendDomainHom f) _ _

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

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

Разделы

Аффилиация

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