val_zpow

Mathlib.Algebra.Star.SelfAdjoint

URI: https://scilib.ai/kg/mathlib#selfAdjoint.val_zpow

English

The value of x^z in the ambient ring equals the z-power of the value of x.

Русский

Значение x^z в внешнем кольце равно z-ой степени значения x.

LaTeX

$$$\forall x \in \mathrm{selfAdjoint}(R),\forall z \in \mathbb{Z}, \uparrow(x^z) = (\uparrow x)^z$$$

Lean4

@[simp, norm_cast]
theorem val_zpow (x : selfAdjoint R) (z : ℤ) : ↑(x ^ z) = (x : R) ^ z :=
  rfl

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

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

Разделы

Аффилиация

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