mapMatrix_trans — Mathlib

English

The composition of the matrix-coefficient equivalences corresponds to the matrix equivalence of the composed coefficients: applying f then g is the same as applying f ∘ g to every entry.

Русский

Сведение эквивалентностей коэффициентов на матрицах по порядку соответствует сведению коэффициентов, получаемых при композиции: применение f затем g есть то же самое, что применение f ∘ g к каждому элементу.

LaTeX

$$$f.\\mathrm{mapMatrix} \\circ g.\\mathrm{mapMatrix} = (f \\circ g).\\mathrm{mapMatrix}$$$

Lean4

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

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