zpow — Mathlib

English

If x is self-adjoint in a group with star, then x^n is self-adjoint for all integers n.

Русский

Если x самосопряжён в группе с звездой, то x^n самосопряжён для всех целых n.

LaTeX

$$$\text{IsSelfAdjoint}(x) \rightarrow \forall n \in \mathbb{Z}, \text{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]

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