zpow_neg_one — Mathlib

English

For any square matrix A with invertible determinant, A^{(-1)} equals the inverse matrix A^{-1}. In other words, A raised to minus one is the inverse of A.

Русский

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

LaTeX

$$$$A^{-1} = A^{(-1)}.$$$$

Lean4

@[simp]
theorem zpow_neg_one (A : M) : A ^ (-1 : ℤ) = A⁻¹ :=
  by
  convert DivInvMonoid.zpow_neg' 0 A
  simp only [zpow_one, Int.ofNat_zero, Int.natCast_succ, zpow_eq_pow, zero_add]

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