mapMatrix_id — Mathlib

English

The identity coefficient homomorphism induces the identity on matrices: mapMatrix of the identity is the identity on matrices.

Русский

Тождественная гомоморфность коэффициентов индуцирует тождественную на матрицах: mapMatrix от тождества равен тождеству над матрицами.

LaTeX

$$$(\\mathrm{AddMonoidHom.id}\\ α).\\mathrm{mapMatrix} = \\mathrm{AddMonoidHom.id}(\\mathrm{Matrix}\\ m\\ n\\ α) $$$

Lean4

@[simp]
theorem mapMatrix_id : (AddMonoidHom.id α).mapMatrix = AddMonoidHom.id (Matrix m n α) :=
  rfl

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