adjugate_pow — Mathlib

English

Let A be an n×n matrix over a commutative ring. For every natural number k, the adjugate of A raised to the k-th power equals the k-th power of the adjugate of A: adj(A^k) = (adj A)^k.

Русский

Пусть A — квадратная матрица размерности n над коммутативным кольцом. Для любого натурального k выполняется adj(A^k) = (adj A)^k.

LaTeX

$$$\\operatorname{adj}(A^k) = \\operatorname{adj}(A)^k$$$

Lean4

@[simp]
theorem adjugate_pow (A : Matrix n n α) (k : ℕ) : adjugate (A ^ k) = adjugate A ^ k := by
  induction k with
  | zero => simp
  | succ k IH => rw [pow_succ', adjugate_mul_distrib, IH, pow_succ]

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