charmatrix_map — Mathlib

English

The charmatrix commutes with entrywise ring homomorphisms: charmatrix(M.map f) = charmatrix(M).map (Polynomial.map f).

Русский

Характеристическая матрица коммутирует отображение по входам матрицы: charmatrix(M.map f) = charmatrix(M).map (Polynomial.map f).

LaTeX

$$$\operatorname{charmatrix}(M.map f) = \bigl(\operatorname{charmatrix}(M)\bigr).map (\operatorname{Polynomial.map} f)$$

Lean4

theorem charmatrix_map (M : Matrix n n R) (f : R →+* S) :
    charmatrix (M.map f) = (charmatrix M).map (Polynomial.map f) :=
  by
  ext i j
  by_cases h : i = j <;> simp [h, charmatrix, diagonal]

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