mapMatrix_refl — Mathlib

English

Identity additive equivalence induces identity on matrix space: (AddEquiv.refl α).mapMatrix = AddEquiv.refl (Matrix m n α).

Русский

Тождественная аддитивная эквивалентность на коэффициентах порождает тождественную эквивалентность на матрицах: (AddEquiv.refl α).mapMatrix = AddEquiv.refl (Matrix m n α).

LaTeX

$$$(\\mathrm{AddEquiv.refl}\\ α).\\mathrm{mapMatrix} = \\mathrm{AddEquiv.refl}(\\mathrm{Matrix}\\ m\\ n\\ α).$$$

Lean4

@[simp]
theorem mapMatrix_refl : (AddEquiv.refl α).mapMatrix = AddEquiv.refl (Matrix m n α) :=
  rfl

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