inv_pow' — Mathlib

English

For a square matrix A and a natural number n, (A^{-1})^{n} = (A^{n})^{-1}. In particular, A^{-1}^n equals the inverse of A^n.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem inv_pow' (A : M) (n : ℕ) : A⁻¹ ^ n = (A ^ n)⁻¹ := by
  induction n with
  | zero => simp
  | succ n ih => rw [pow_succ A, mul_inv_rev, ← ih, ← pow_succ']

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