map_mul — Mathlib

English

For ring hom f: α → β, the entrywise map preserves multiplication of matrices: map f (L · M) = map f L · map f M.

Русский

При отображении по кольцам f: α → β сохраняется умножение матриц: map f (L M) = map f L · map f M.

LaTeX

$$$ (\\operatorname{map} f) (L M) = (\\operatorname{map} f L) \\cdot (\\operatorname{map} f M) $$$

Lean4

@[simp]
protected theorem map_mul [Fintype n] {L : Matrix m n α} {M : Matrix n o α} [NonAssocSemiring β] {f : α →+* β} :
    (L * M).map f = L.map f * M.map f := by
  ext
  simp [mul_apply, map_sum]

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