toLin_toMatrix — Mathlib

English

For any linear map f : M1 → M2, converting f to a matrix and then back to a linear map returns f, i.e., Matrix.toLin v1 v2 (LinearMap.toMatrix v1 v2 f) = f.

Русский

Для линейного отображения f: M1 → M2 преобразование в матрицу, а затем обратно в линейное отображение даёт исходное отображение f.

LaTeX

$$$\\text{Matrix.toLin } v_1 v_2 (\\text{LinearMap.toMatrix } v_1 v_2 f) = f.$$$

Lean4

@[simp]
theorem toLin_toMatrix (f : M₁ →ₗ[R] M₂) : Matrix.toLin v₁ v₂ (LinearMap.toMatrix v₁ v₂ f) = f := by
  rw [← Matrix.toLin_symm, LinearEquiv.apply_symm_apply]

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