val_pow

Mathlib.Algebra.Star.SelfAdjoint

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

English

The value in R of x^n equals the n-th power of the value of x.

Русский

Обратно к значению в R: x^n в подтипе соответсвует (x)^n в R.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem val_pow (x : selfAdjoint R) (n : ℕ) : ↑(x ^ n) = (x : R) ^ n :=
  rfl

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

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

Разделы

Аффилиация

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