matPolyEquiv_map_smul — Mathlib

English

The map matPolyEquiv distributes scalar polynomials: matPolyEquiv(p·M) equals the product of (Polynomial.map ... p) and matPolyEquiv M.

Русский

Умножение матрицы на полином слева переносится через matPolyEquiv как произведение соответствующих отображённых полиномов и matPolyEquiv M.

LaTeX

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

Lean4

@[simp]
theorem matPolyEquiv_map_smul (p : R[X]) (M : Matrix n n R[X]) :
    matPolyEquiv (p • M) = p.map (algebraMap _ _) * matPolyEquiv M := by
  rw [← one_mul M, ← smul_mul_assoc, map_mul, matPolyEquiv_smul_one, one_mul]

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