mapMatrix_refl — Mathlib

English

The identity AlgEquiv on α yields the identity AlgEquiv on matrices: AlgEquiv.refl.mapMatrix = (AlgEquiv.refl : Matrix m m α ≃ₐ[R] _).

Русский

Идентичное AlgEquiv на α порождает идентичный AlgEquiv на матрицах: AlgEquiv.refl.mapMatrix = (AlgEquiv.refl : Matrix m m α ≃ₐ[R] _).

LaTeX

$$$\text{AlgEquiv.refl.mapMatrix} = (\text{AlgEquiv.refl} : \mathrm{Matrix}_{m\times m}(\alpha) \simeq_{\mathrm{Alg}} _)$$$

Lean4

@[simp]
theorem mapMatrix_refl : AlgEquiv.refl.mapMatrix = (AlgEquiv.refl : Matrix m m α ≃ₐ[R] _) :=
  rfl

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