English
Mutual invertibility of the matrix-to-linear-map correspondence implies that changing bases via a linear equivalence yields the corresponding conjugation of the matrix representation.
Русский
Взаимная обратимость соответствия между матрицами и линейными отображениями означает, что переход базисов через линейное эквививалентное отображение приводит к соответствующему сопряжению матричного представления.
LaTeX
$$$\\text{toMatrix}_{v_1,v_2} (f) \\mapsto \\text{toLin}_{v_1,v_2} (f)$ взаимно обратны; соответствие сохраняет структуру при заменах базисов.$$
Lean4
@[simp]
theorem toMatrix_toLin (M : Matrix m n R) : LinearMap.toMatrix v₁ v₂ (Matrix.toLin v₁ v₂ M) = M := by
rw [← Matrix.toLin_symm, LinearEquiv.symm_apply_apply]
