map_vecMul — Mathlib

English

Let f be a ring homomorphism and M a matrix. Then f maps the vecMul with v to the vecMul with f∘v on the mapped matrix: f(v ᵥ* M) = (f∘v) ᵥ* M.map f.

Русский

Пусть f — кольцевой гомоморф, и M — матрица. Тогда f( v ᵥ* M ) = (f∘v) ᵥ* (M.map f).

LaTeX

$$$\\text{Let } f: α\\to β, \\; M\\in M_{n\\times m}(α), \\; v: n\\to α.\\quad f(v ᵥ* M) = (f\\circ v) ᵥ* M.map f.$$$

Lean4

theorem map_vecMul [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (M : Matrix n m R) (v : n → R) (i : m) :
    f ((v ᵥ* M) i) = ((f ∘ v) ᵥ* M.map f) i := by
  simp only [Matrix.vecMul, Matrix.map_apply, RingHom.map_dotProduct, Function.comp_def]

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