mapMatrix_id — Mathlib

English

The matrix-map induced by the identity algebra homomorphism is the identity on matrices.

Русский

Матричное отображение, индуцированное тождественным алгебраическим отображением, является тождественным отображением на матрицах.

LaTeX

$$$(\mathrm{AlgHom.id}\ R \alpha).mapMatrix = \mathrm{AlgHom.id}\ R (\mathrm{Matrix}_{m\times m}(\alpha))$$$

Lean4

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

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