mapMatrix_trans — Mathlib

English

Composition of additive equivalences corresponds to the matrix-level composition: f.mapMatrix.trans g.mapMatrix = ((f.trans g).mapMatrix).

Русский

Сведение аддитивных эквивалентностей на уровне матриц соответствует композиции эквивалентностей коэффициентов: f.mapMatrix.trans g.mapMatrix = ((f.trans g).mapMatrix).

LaTeX

$$$f.mapMatrix.trans g.mapMatrix = ((f.trans g).mapMatrix)$$$

Lean4

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

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