extendDomain_pow

Mathlib.Algebra.Group.End

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

English

For 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_pow (n : ℕ) : (e ^ n).extendDomain f = e.extendDomain f ^ n :=
  map_pow (extendDomainHom f) _ _

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

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

Разделы

Аффилиация

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