charmatrix_diagonal — Mathlib

English

If p is a diagonal matrix from polynomials, charmatrix(p) is diagonal with entries X − p_i on the diagonal.

Русский

Если p — диагональная матрица полиномов, charmatrix(p) диагональная с диагональными элементами X − p_i.

LaTeX

$$$\text{charmatrix}(\text{diag}(p)) = \text{diag}(X - p_i)$$$

Lean4

@[simp]
theorem charmatrix_diagonal (d : n → R) : charmatrix (diagonal d) = diagonal fun i => X - C (d i) := by
  rw [charmatrix, scalar_apply, RingHom.mapMatrix_apply, diagonal_map (map_zero _), diagonal_sub]

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