map_matrix_mul — Mathlib

English

Let f be a ring homomorphism between semirings α and β, and M ∈ M_{m×n}(α), N ∈ M_{n×o}(α). Then f preserves matrix multiplication: f(MN) = f(M) f(N) under the usual map on entries.

Русский

Пусть f — кольцевой гомоморфизм между полями α и β; для матриц M и N верно: f(MN) = f(M) f(N).

LaTeX

$$$\\text{If } f: α \\to β \\,\\text{is a ring homomorphism and } M \\in M_{m\\times n}(α), N \\in M_{n\\times o}(α), \\; f(MN) = f(M) f(N).$$$

Lean4

theorem map_matrix_mul (M : Matrix m n α) (N : Matrix n o α) (i : m) (j : o) (f : α →+* β) :
    f ((M * N) i j) = (M.map f * N.map f) i j := by simp [Matrix.mul_apply, map_sum]

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