toMvPolynomial_map — Mathlib

English

The mv-polynomial associated to the matrix after applying a ring hom f coordinatewise equals applying f to the polynomial associated to the matrix; i.e., map f to M toMvPolynomial equals M.toMvPolynomial mapped by f.

Русский

mv-полиномы, ассоциированные с матрицей после применения кольцевого отображения f по координатам, равны применению f к полиномe, ассоциированному с матрицей.

LaTeX

$$(M.map f).toMvPolynomial i = MvPolynomial.map f (M.toMvPolynomial i)$$

Lean4

theorem toMvPolynomial_map (f : R →+* S) (M : Matrix m n R) (i : m) :
    (M.map f).toMvPolynomial i = MvPolynomial.map f (M.toMvPolynomial i) := by
  simp only [toMvPolynomial, map_apply, map_sum, map_monomial]

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