matPolyEquiv_smul_one — Mathlib

English

The map matPolyEquiv respects multiplication by a polynomial on the left by turning it into a matrix multiple on the right by the algebra map.

Русский

Отображение matPolyEquiv сохраняет умножение на полином слева, переводя его в умножение матрицы справа через алгебраическое отображение.

LaTeX

$$$\\text{matPolyEquiv}(p \\;\\cdot\\; I) = p.map (algebraMap R (Matrix n n R))$$$

Lean4

theorem matPolyEquiv_smul_one (p : R[X]) :
    matPolyEquiv (p • (1 : Matrix n n R[X])) = p.map (algebraMap R (Matrix n n R)) :=
  by
  ext m i j
  simp only [matPolyEquiv_coeff_apply, smul_apply, one_apply, smul_eq_mul, mul_ite, mul_one, mul_zero, coeff_map,
    algebraMap_matrix_apply, Algebra.algebraMap_self, RingHom.id_apply]
  split_ifs <;> simp

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