mapMatrix_refl — Mathlib

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

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