mapMatrix_comp — Mathlib

English

For algebra homomorphisms f: β→γ and g: α→β, the matrix-map respects composition: mapMatrix(f) ∘ mapMatrix(g) = mapMatrix(f ∘ g).

Русский

Для отображений f: β→γ и g: α→β композицию отображений матриц соблюдает: mapMatrix(f) ∘ mapMatrix(g) = mapMatrix(f ∘ g).

LaTeX

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

Lean4

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

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