English
For f a ring homomorphism and M a matrix, the map preserves the vecMul with a vector v: f((M mulVec v) i) = (M.map f) mulVec (f ∘ v) i.
Русский
Пусть f — гомоморфизм кольца, M — матрица. Тогда сохранение vecMul: f((M mulVec v) i) = (M.map f) mulVec (f ∘ v) i.
LaTeX
$$$\\text{Let } f: α\\to β, \\; M \\in M_{m\\times n}(α), \\; v: n\\to α, \\; i.\\quad f((M mulVec v)_i) = (M.map f \\; \\, mulVec (f\\circ v))_i.$$$
Lean4
theorem map_mulVec [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (M : Matrix m n R) (v : n → R) (i : m) :
f ((M *ᵥ v) i) = (M.map f *ᵥ (f ∘ v)) i := by
simp only [Matrix.mulVec, Matrix.map_apply, RingHom.map_dotProduct, Function.comp_def]
