zpow — Mathlib

English

If A is Hermitian, then A^k is Hermitian for all integer powers k.

Русский

Если A Гермитова, то A^k Гермитова для любого целого k.

LaTeX

$$A^{k\,\\mathrm{H}} = A^k$$

Lean4

/-- Note that `IsSelfAdjoint.zpow` does not apply to matrices as they are not a division ring. -/
theorem zpow [Fintype m] [DecidableEq m] {A : Matrix m m α} (h : A.IsHermitian) (k : ℤ) : (A ^ k).IsHermitian := by
  rw [IsHermitian, conjTranspose_zpow, h]

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