mapMatrix_comp — Mathlib

English

Composition of coefficient homomorphisms corresponds to composition of their induced matrix homomorphisms: f.mapMatrix ∘ g.mapMatrix = (f ∘ g).mapMatrix.

Русский

Компоновка гомоморфизмов коэффициентов соответствует компоновке их порожденных гомоморфизмов матриц: f.mapMatrix ∘ g.mapMatrix = (f ∘ g).mapMatrix.

LaTeX

$$$f.mapMatrix \\circ g.mapMatrix = (f \\circ g).mapMatrix$$$

Lean4

@[simp]
theorem mapMatrix_comp (f : β →+ γ) (g : α →+ β) :
    f.mapMatrix.comp g.mapMatrix = ((f.comp g).mapMatrix : Matrix m n α →+ _) :=
  rfl

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