conjTranspose_zpow — Mathlib

English

For a matrix over a star-ring, conjugate transpose commutes with z-powers: (A^n)ᴴ = (Aᴴ)^n for all integers n.

Русский

Для матрицы над звездообразным кольцом сопряжённое транспонирование сохраняет z-повер: (A^n)ᴴ = (Aᴴ)^n для всех целых n.

LaTeX

$$$ \forall n \in \mathbb{Z},\ (A^n)^{\ast} = (A^{\ast})^n $$$

Lean4

@[simp]
theorem conjTranspose_zpow [StarRing R] (A : M) : ∀ n : ℤ, (A ^ n)ᴴ = Aᴴ ^ n
  | (n : ℕ) => by rw [zpow_natCast, zpow_natCast, conjTranspose_pow]
  | -[n+1] => by rw [zpow_negSucc, zpow_negSucc, conjTranspose_nonsing_inv, conjTranspose_pow]

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