instPowSubtypeMemAddSubgroupNat

Mathlib.Algebra.Star.SelfAdjoint

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

English

Power by natural numbers on self-adjoint elements respects structure.

Русский

Возведение самосопряжённых элементов в степень по натуральному числу сохраняет структуру.

LaTeX

$$$\forall x \in \mathrm{selfAdjoint}(R),\forall n \in \mathbb{N}, x^n \text{ определено как в } R$$$

Lean4

instance : Pow (selfAdjoint R) ℕ where pow x n := ⟨(x : R) ^ n, x.prop.pow n⟩

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

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

Разделы

Аффилиация

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