inv_zpow — Mathlib

English

For any square matrix A, A^{-1}^{n} = (A^{n})^{-1} for all integers n, provided det(A) is a unit; i.e., the inverse of a z-power equals the z-power of the inverse.

Русский

Для любой квадратной матрицы A верно A^{-1}^{n} = (A^{n})^{-1} для всех целых n, если det(A) является единичным.

LaTeX

$$$$A^{-1}^{n} = (A^{n})^{-1} \\quad (n \\in \\mathbb{Z}), \\text{ при } \\det(A) \\in \\mathbb{R}^{\\times}. $$$$

Lean4

theorem inv_zpow (A : M) : ∀ n : ℤ, A⁻¹ ^ n = (A ^ n)⁻¹
  | (n : ℕ) => by rw [zpow_natCast, zpow_natCast, inv_pow']
  | -[n+1] => by rw [zpow_negSucc, zpow_negSucc, inv_pow']

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