coe_zpow

Mathlib.Algebra.Star.Unitary

URI: https://scilib.ai/kg/mathlib#unitary.coe_zpow

English

For U ∈ unitary R and z ∈ Z, the embedding commutes with integer powers: ↑(U^z) = (U^z).

Русский

Для U ∈ unitary R и z ∈ Z вложение коммутирует с целочисленными степенями: ↑(U^z) = (U^z).

LaTeX

$$$\uparrow (U^z) = (U^z)$$$

Lean4

@[norm_cast]
theorem coe_zpow (U : unitary R) (z : ℤ) : ↑(U ^ z) = (U : R) ^ z :=
  by
  cases z
  · simp [SubmonoidClass.coe_pow]
  · simp [coe_inv]

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

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

Разделы

Аффилиация

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