zpow₀ — Mathlib

English

Let x be self-adjoint in a star-algebra with zero. Then for every integer n, x^n is self-adjoint.

Русский

Пусть x — самосопряжённый элемент в звёздной алгебре с нулём. Тогда для любого целого числа n элемент x^n также самосопряжён.

LaTeX

$$$IsSelfAdjoint(x) \rightarrow \forall n \in \mathbb{Z},\ IsSelfAdjoint(x^n)$$$

Lean4

@[aesop safe apply]
theorem zpow₀ {x : R} (hx : IsSelfAdjoint x) (n : ℤ) : IsSelfAdjoint (x ^ n) := by
  simp only [isSelfAdjoint_iff, star_zpow₀, hx.star_eq]

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