mapMatrix_comp — Mathlib

English

A RingEquiv f: α ≃+* β induces a RingEquiv between square matrices: mapMatrix(f): Matrix m m α ≃+* Matrix m m β, acting entrywise.

Русский

Кольцевое эквивалентное отображение f: α ≃+* β порождает кольцевое эквивалентное отображение между квадратными матрицами: mapMatrix(f): Mat_{m×m}(α) ≃+* Mat_{m×m}(β), действующее по элементам.

LaTeX

$$$\text{mapMatrix}(f) : M_{m\times m}(\alpha) \cong_{\text{ring}} M_{m\times m}(\beta), \; [\text{mapMatrix}(f)(M)]_{ij} = f(M_{ij}).$$$

Lean4

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

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