inv_zpow' — Mathlib

English

For a square matrix A with det(A) a unit, (A^{-1})^{n} = (A^{n})^{-1} for all integers n. The inverse of a z-power equals the z-power of the inverse.

Русский

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

LaTeX

$$$$ (A^{-1})^{n} = (A^{n})^{-1} \\quad (n\\in\\mathbb{Z}) $$$$

Lean4

theorem inv_zpow' {A : M} (h : IsUnit A.det) (n : ℤ) : A⁻¹ ^ n = A ^ (-n) := by rw [zpow_neg h, inv_zpow]

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