transpose_zpow — Mathlib

English

For any matrix A, transpose commutes with z-powers: (A^n)^T = (A^T)^n for all integers n.

Русский

Для любой матрицы A транспонирование сохраняет z-поразряды: (A^n)^T = (A^T)^n при всех целых n.

LaTeX

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

Lean4

@[simp]
theorem transpose_zpow (A : M) : ∀ n : ℤ, (A ^ n)ᵀ = Aᵀ ^ n
  | (n : ℕ) => by rw [zpow_natCast, zpow_natCast, transpose_pow]
  | -[n+1] => by rw [zpow_negSucc, zpow_negSucc, transpose_nonsing_inv, transpose_pow]

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