diagonal_pow — Mathlib

English

For a finite set n and a function v: n → α, the k-th power of the diagonal matrix diag(v) is diag(v^k).

Русский

Для функции v: n → α и целочисленного k, диагональная матрица diag(v) в степени k равна diag(v^k).

LaTeX

$$$\\operatorname{diag}(v)^k = \\operatorname{diag}(v^k)$$$

Lean4

theorem diagonal_pow [Fintype n] [DecidableEq n] (v : n → α) (k : ℕ) : diagonal v ^ k = diagonal (v ^ k) :=
  (map_pow (diagonalRingHom n α) v k).symm

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