mapMatrix_trans — Mathlib

English

For AlgEquiv f: α ≃ₐ[R] β and g: β ≃ₐ[R] γ, the matrix-map of the composed is equal to the matrix-map of the composition: f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix.

Русский

Для AlgEquiv f: α ≃ₐ[R] β и g: β ≃ₐ[R] γ выполняется: mapMatrix(f).trans mapMatrix(g) = mapMatrix(f.trans g).

LaTeX

$$$f.mapMatrix.trans g.mapMatrix = ((f.trans g).mapMatrix : Matrix m m α ≃ₐ[R] _)$$$

Lean4

@[simp]
theorem mapMatrix_trans (f : α ≃ₐ[R] β) (g : β ≃ₐ[R] γ) :
    f.mapMatrix.trans g.mapMatrix = ((f.trans g).mapMatrix : Matrix m m α ≃ₐ[R] _) :=
  rfl

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