English
The identity equivalence on the coefficient space induces the identity equivalence on the matrix space: applying the identity to entries yields no change to the matrix.
Русский
Тождественная эквивалентность на пространстве коэффициентов порождает тождественную эквивалентность для пространства матриц: применение тождественного к элементам не изменяет матрицу.
LaTeX
$$$(\\mathrm{Equiv\\,refl}\\,\\alpha).\\mathrm{mapMatrix} = \\mathrm{Equiv\\,refl}(\\mathrm{Matrix}\\, m\\, n\\, \\alpha).$$$
Lean4
@[simp]
theorem mapMatrix_refl : (Equiv.refl α).mapMatrix = Equiv.refl (Matrix m n α) :=
rfl