coe_ofLinearEquiv — Mathlib

English

The underlying function of Matrix.ofLinearEquiv coincides with the natural identification; the coercion of the linear equivalence is exactly the canonical correspondence.

Русский

Базовая функция Matrix.ofLinearEquiv совпадает с естественным отображением; отображение по умолчанию совпадает с каноническим соответствием.

LaTeX

$$$\\bigl\\langle Matrix.ofLinearEquiv \\bigr\\rangle = \\text{of}$$$

Lean4

@[simp]
theorem coe_ofLinearEquiv [Semiring R] [AddCommMonoid α] [Module R α] :
    ⇑(ofLinearEquiv _ : (m → n → α) ≃ₗ[R] Matrix m n α) = of :=
  rfl

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