zpow_neg_natCast — Mathlib

English

For any square matrix A, and natural n, A^{(-n)} = (A^{n})^{-1}. This expresses the negative z-powers as inverses of positive powers.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem zpow_neg_natCast (A : M) (n : ℕ) : A ^ (-n : ℤ) = (A ^ n)⁻¹ :=
  by
  cases n
  · simp
  · exact DivInvMonoid.zpow_neg' _ _

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