mapMatrix_id — Mathlib

English

If f: β → γ and g: α → β are ring homomorphisms, then 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_id : (RingHom.id α).mapMatrix = RingHom.id (Matrix m m α) :=
  rfl

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