toLinearMap₂'Aux_toMatrix₂Aux

English

The forward and reverse constructions between matrices and bilinear maps compose to the identity on both sides.

Русский

Составления прямого и обратного преобразований между матрицами и билинейными отображениями дают тождество с обеих сторон.

LaTeX

$$$\text{(toLinearMap₂'Aux) ∘ (toMatrix₂Aux) = id}$ and $\text{(toMatrix₂Aux) ∘ (toLinearMap₂'Aux) = id}$$$

Lean4

theorem toLinearMap₂'Aux_toMatrix₂Aux (f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) :
    Matrix.toLinearMap₂'Aux σ₁ σ₂ (LinearMap.toMatrix₂Aux R (fun i => Pi.single i 1) (fun j => Pi.single j 1) f) = f :=
  by
  refine ext_basis (Pi.basisFun R₁ n) (Pi.basisFun R₂ m) fun i j => ?_
  simp_rw [Pi.basisFun_apply, Matrix.toLinearMap₂'Aux_single, LinearMap.toMatrix₂Aux_apply]

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