English
The matrix acts as a linear equivalence between matrices and the corresponding linear maps, establishing a bijection.
Русский
Матрица задаёт двустороннюю линейную эквиваленцию между матрицами и соответствующими линейными отображениями.
LaTeX
$$def toLin' : Matrix m n R ≃ₗ[R] (n → R) →ₗ[R] m → R$$
Lean4
/-- Linear maps `(n → R) →ₗ[R] (m → R)` are linearly equivalent to `Matrix m n R`. -/
def toMatrix' : ((n → R) →ₗ[R] m → R) ≃ₗ[R] Matrix m n R
where
toFun f := of fun i j ↦ f (Pi.single j 1) i
invFun := Matrix.mulVecLin
right_inv
M := by
ext i j
simp only [Matrix.mulVec_single_one, col_apply, Matrix.mulVecLin_apply, of_apply]
left_inv
f := by
apply (Pi.basisFun R n).ext
intro j; ext i
simp only [Pi.basisFun_apply, Matrix.mulVec_single_one, col_apply, Matrix.mulVecLin_apply, of_apply]
map_add' f
g := by
ext i j
simp only [Pi.add_apply, LinearMap.add_apply, of_apply, Matrix.add_apply]
map_smul' c
f := by
ext i j
simp only [Pi.smul_apply, LinearMap.smul_apply, RingHom.id_apply, of_apply, Matrix.smul_apply]
